A semantic normalization proof for a system with recursors

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 extend to prove strong normalization results, in particular for theories in deduction modulo. However such semantic methods did not apply for systems with recursors like Godel system T. We show in this paper how super natural deduction provides a bridge between superconsistency of arithmetic and strong normalization of system T. We then generalize this result to a family of inductive types before discussing the dependant case.
Type de document :
Pré-publication, Document de travail
2008
Liste complète des métadonnées

Littérature citée [28 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00211877
Contributeur : Paul Brauner <>
Soumis le : mardi 22 janvier 2008 - 10:29:31
Dernière modification le : jeudi 10 mai 2018 - 02:06:56
Document(s) archivé(s) le : jeudi 15 avril 2010 - 01:56:27

Fichiers

paper.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00211877, version 1

Collections

Citation

Lisa Allali, Paul Brauner. A semantic normalization proof for a system with recursors. 2008. 〈inria-00211877〉

Partager

Métriques

Consultations de la notice

241

Téléchargements de fichiers

151