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.
Type de document :
Communication dans un congrès
25th Annual IEEE Symposium on Logic in Computer Science (LICS 2010), Jul 2010, Edinburgh, United Kingdom. 2010
Liste complète des métadonnées

https://hal.inria.fr/inria-00516858
Contributeur : Jian-Qi Li <>
Soumis le : dimanche 12 septembre 2010 - 17:32:06
Dernière modification le : mardi 17 avril 2018 - 11:28:11

Identifiants

  • HAL Id : inria-00516858, version 1

Collections

Citation

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

Partager

Métriques

Consultations de la notice

164