Skip to Main content Skip to Navigation
New interface
Conference papers

A Computability Path Ordering for Polymorphic Terms

Jean-Pierre Jouannaud 1, * Jian-Qi Li 1, 2 
* Corresponding author
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 : Monday, July 5, 2010 - 5:40:57 AM
Last modification on : Thursday, February 3, 2022 - 11:18:10 AM


  • HAL Id : inria-00497405, version 1



Jean-Pierre Jouannaud, Jian-Qi Li. A Computability Path Ordering for Polymorphic Terms. 11th International Workshop on Termination, Jul 2010, Edinburgh, United Kingdom. ⟨inria-00497405⟩



Record views