28596 articles – 22090 Notices  [english version]

inria-00073135, version 1

A Generic Normalisation Proof for Pure Type Systems

paul-andré melliès, Benjamin Werner () 1

N° RR-3548 (1998)

Résumé : We prove the strong normalisation for any PTS, provided the existence of a certain $\Lambda$-set $\A for every sort s of the system. The properties verified by the $\A's depend of the axioms and rules of the type system. A slightly shortened version of this work has been published under the same title in the volume «Types for Proofs and Programs», Internatio- nal workshop TYPES'96, E. Gimenez and C. Paulin-Mohring Eds, LNCS 1512, Springer-Verlag, 1998.

  • 1 :  COQ (INRIA Rocquencourt)
  • INRIA
  • Domaine : Informatique/Autre
  • Mots-clés : TYPE THEORY / LAMBDA-CALCULUS / NORMALIZATION
  • Référence interne : RR-3548
  • Commentaire : Projet COQ
 
  • inria-00073135, version 1
  • http://hal.inria.fr/inria-00073135
  • oai:hal.inria.fr:inria-00073135
  • Contributeur : Rapport De Recherche Inria <>
  • Soumis le : Mercredi 24 Mai 2006, 11:57:32
  • Dernière modification le : Mercredi 18 Avril 2007, 11:04:50