A Semantic Normalization Proof for Inductive Types

Lisa Allali (1) , Paul Brauner (2)

1 LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
2 PAREO - Formal islands: foundations and applications

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.

Mots clés: deduction modulo; normalization; superconsistency; inductive types; recursors

Domaines: Logique en informatique [cs.LO]

Lisa Allali, Paul Brauner. A Semantic Normalization Proof for Inductive Types. [Research Report] 2008, pp.21. ⟨inria-00280410v2⟩