inria-00516858, version 1
A Computability Path Ordering for Polymorphic Terms - Short Paper
Jian-Qi Li
1, 2
25th Annual IEEE Symposium on Logic in Computer Science (LICS 2010) (2010)
Résumé : 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.
- 1 : FORMES (LIAMA)
- INRIA – Tsinghua University / Beijing – LIAMA
- 2 : Tsinghua University
- Tsinghua University
- Domaine : Informatique/Logique en informatique
- Mots-clés : strong normalisation – system F – higher-order rules – computability path ordering
- inria-00516858, version 1
- http://hal.inria.fr/inria-00516858
- oai:hal.inria.fr:inria-00516858
- Contributeur : Jian-Qi Li
- Soumis le : Dimanche 12 Septembre 2010, 17:32:06
- Dernière modification le : Lundi 13 Septembre 2010, 11:22:22
Exporter