Abstract : We develop a new version of the computability path ordering, which is well-founded on the set of polymorphic lambda terms. This is a new important step towards our challenge: to develop a well-founded order on the set of terms of the calculus of constructions, allowing to reduce strong normalization proofs of logical calculi to ordering comparisons of their computational rules.
https://hal.inria.fr/inria-00516858
Contributeur : Jian-Qi Li
<>
Soumis le : dimanche 12 septembre 2010 - 17:32:06
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Jian-Qi Li. A Computability Path Ordering for Polymorphic Terms - Short Paper. 25th Annual IEEE Symposium on Logic in Computer Science (LICS 2010), Jul 2010, Edinburgh, United Kingdom. 2010. 〈inria-00516858〉
