Name
Abstract | ||
|---|---|---|
In this paper, we first briefly survey automated termination proof methods for higher-order calculi. We then concentrate on the higher-order recursive path ordering, for which we provide an improved definition, the Computability Path Ordering. This new definition appears indeed to capture the essence of computability arguments à la Tait and Girard, therefore explaining the name of the improved ordering. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1007/978-3-540-87531-4_1 | computer science logic |
Keywords | DocType | Volume |
computability argument,la tait,briefly survey automated termination,proof method,computability path ordering,improved definition,higher-order calculus,new definition,higher-order recursive path,termination,rewriting,lambda calculus,higher order | Conference | abs/0806.2517 |
ISSN | Citations | PageRank |
0302-9743 | 19 | 0.74 |
References | Authors | |
46 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Frédéric Blanqui | 1 | 290 | 17.96 |
| Jean-Pierre Jouannaud | 2 | 1921 | 227.43 |
| Albert Rubio | 3 | 228 | 19.44 |