The Calculus of explicit substitutions lambda-upsilon

Abstract : lambda-upsilon-calculus is a new simple calculus of explicit substitutions. In the paper we explore its properties, namely we prove that it correctly implements B reduction, it is confluent, its simply typed version is strongly normalizing. We associate with it an abstract machine called the U-machine. We prove that it is a correct implementation of the calculus.
Type de document :
Rapport
[Research Report] RR-2222, INRIA. 1994
Liste complète des métadonnées

https://hal.inria.fr/inria-00074448
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 15:19:14
Dernière modification le : samedi 17 septembre 2016 - 01:06:53
Document(s) archivé(s) le : mardi 12 avril 2011 - 17:00:33

Fichiers

Identifiants

  • HAL Id : inria-00074448, version 1

Collections

Citation

Pierre Lescanne, Jocelyne Rouyer-Degli. The Calculus of explicit substitutions lambda-upsilon. [Research Report] RR-2222, INRIA. 1994. 〈inria-00074448〉

Partager

Métriques

Consultations de la notice

106

Téléchargements de fichiers

61