Skip to Main content Skip to Navigation
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

https://hal.inria.fr/inria-00497405
Contributor : Jian-Qi Li <>
Submitted on : Monday, July 5, 2010 - 5:40:57 AM
Last modification on : Wednesday, June 2, 2021 - 3:39:52 AM

Identifiers

  • HAL Id : inria-00497405, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

263