Skip to Main content Skip to Navigation
Conference papers

A Computability Path Ordering for Polymorphic Terms - Short Paper

Jian-Qi Li 1, 2 
1 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
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.
Document type :
Conference papers
Complete list of metadata
Contributor : Jian-Qi Li Connect 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


  • HAL Id : inria-00516858, version 1



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⟩



Record views