inria-00280410, version 2
A Semantic Normalization Proof for Inductive Types
Lisa Allali a, 1Paul Brauner
2
(2008)
Résumé : Semantics methods have been used to prove cut elimination theorems for a long time. It is only recently that they have been extended to prove strong normalization results. For instance using the notion of super-consistency that is a semantic criterion for theories expressed in deduction modulo implying strong normalization. However, the strong normalization of System T has always been reluctant to such semantic methods. In this paper we give a semantic normalization proof of system T using the super consistency of some theory. We then extend the result to every strictly positive inductive type and discuss the extension to predicate logic.
- a – INRIA
- 1 : Laboratoire d'informatique de l'école polytechnique (LIX)
- CNRS : UMR7161 – Polytechnique - X
- 2 : PAREO (INRIA Lorraine - LORIA)
- INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
- Domaine : Informatique/Logique en informatique
- Mots-clés : deduction modulo – normalization – superconsistency – inductive types – recursors
- Versions disponibles : v1 (17-05-2008) v2 (19-05-2008)
- inria-00280410, version 2
- http://hal.inria.fr/inria-00280410
- oai:hal.inria.fr:inria-00280410
- Contributeur : Paul Brauner
- Soumis le : Lundi 19 Mai 2008, 13:55:39
- Dernière modification le : Lundi 6 Octobre 2008, 15:32:38