Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, Epiciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation

A Semantic Normalization Proof for Inductive Types

Lisa Allali 1 Paul Brauner 2 
2 PAREO - Formal islands: foundations and applications
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : 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.
Document type :
Complete list of metadata

Cited literature [30 references]  Display  Hide  Download
Contributor : Brauner Paul Connect in order to contact the contributor
Submitted on : Monday, May 19, 2008 - 1:55:39 PM
Last modification on : Wednesday, February 2, 2022 - 3:51:17 PM
Long-term archiving on: : Friday, November 25, 2016 - 9:58:45 PM


Files produced by the author(s)


  • HAL Id : inria-00280410, version 2



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



Record views


Files downloads