A Computability Path Ordering for Polymorphic Terms

Jean-Pierre Jouannaud 1, * Jian-Qi Li 1, 2
* Auteur correspondant
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.
Type de document :
Communication dans un congrès
11th International Workshop on Termination, Jul 2010, Edinburgh, United Kingdom. 2010
Liste complète des métadonnées

https://hal.inria.fr/inria-00497405
Contributeur : Jian-Qi Li <>
Soumis le : lundi 5 juillet 2010 - 05:40:57
Dernière modification le : vendredi 25 mai 2018 - 12:02:06

Identifiants

  • 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. 2010. 〈inria-00497405〉

Partager

Métriques

Consultations de la notice

187