s'authentifier
version française rss feed

inria-00280410, version 2

A Semantic Normalization Proof for Inductive Types

Lisa Allali () a1, Paul 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.

  • 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
  • oai:hal.inria.fr:inria-00280410
  • Contributeur : 
  • Soumis le : Lundi 19 Mai 2008, 13:55:39
  • Dernière modification le : Lundi 6 Octobre 2008, 15:32:38
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
  翻译: