Carregant...
Carregant...

Vés al contingut (premeu Retorn)

The computability path ordering

Autor
Blanqui, F.; Jouannaud, J.; Rubio, A.
Tipus d'activitat
Article en revista
Revista
Logical methods in computer science
Data de publicació
2015-10-26
Volum
11
Número
4, Paper 3
Pàgina inicial
1
Pàgina final
45
DOI
10.2168/LMCS-11(4:3)2015
Projecte finançador
DAMAS (TIN2013-45732-C4-3-P)
Repositori
http://arxiv.org/abs/1506.03943 Obrir en finestra nova
http://hdl.handle.net/2117/85100 Obrir en finestra nova
URL
http://www.lmcs-online.org/ojs/viewarticle.php?id=1575 Obrir en finestra nova
Resum
This paper aims at carrying out termination proofs for simply typed higher-order calculi automatically by using ordering comparisons. To this end, we introduce the computability path ordering (CPO), a recursive relation on terms obtained by lifting a precedence on function symbols. A first version, core CPO, is essentially obtained from the higher-order recursive path ordering (HORPO) by eliminating type checks from some recursive calls and by incorporating the treatment of bound variables as in...
Citació
Blanqui, F., Jouannaud, J., Rubio, A. The computability path ordering. "Logical methods in computer science", 26 Octubre 2015, vol. 11, núm. 4, Paper 3, p. 1-45.
Paraules clau
Inductive types, Lambda-calculus, Path order, Red ucibility, Rewriting, Termination
Grup de recerca
LOGPROG - Lògica i Programació

Participants

Arxius