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 Contributor : Jian-Qi LiConnect in order to contact the contributor Submitted on : Sunday, September 12, 2010 - 5:32:06 PM Last modification on : Thursday, February 3, 2022 - 11:18:54 AM
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. ⟨inria-00516858⟩