A Semantic Normalization Proof for Inductive Types - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2008

A Semantic Normalization Proof for Inductive Types

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 normaliza- tion proof of system T using the super consistency of some theory.
Fichier principal
Vignette du fichier
paper.pdf (187.33 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

inria-00280410 , version 1 (17-05-2008)
inria-00280410 , version 2 (19-05-2008)

Identifiants

  • HAL Id : inria-00280410 , version 1

Citer

Lisa Allali, Paul Brauner. A Semantic Normalization Proof for Inductive Types. [Research Report] 2008, pp.21. ⟨inria-00280410v1⟩
185 Consultations
80 Téléchargements

Partager

Gmail Facebook X LinkedIn More