Un Lambda-Calcul Atomique

Résumé : Nous introduisons un lambda-calcul avec partage explicite, le lambda-calcul atomique, dans lequel la duplication des sous-termes est faite pas à pas en fonction des constructeurs. Nous donnons une fonction de dénotation du lambda-calcul atomique dans le lambda-calcul et montrons que le lambda-calcul atomique simule la -réduction et préserve la normalisation forte. Nous donnons aussi un système de type pour le lambda-calcul atomique et montrons que la réduction préserve le type.
Type de document :
Communication dans un congrès
Damien Pous and Christine Tasson. JFLA - Journées francophones des langages applicatifs, Feb 2013, Aussois, France. 2013
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00779903
Contributeur : Ist Inria Saclay <>
Soumis le : mardi 22 janvier 2013 - 16:57:26
Dernière modification le : jeudi 10 mai 2018 - 02:06:54
Document(s) archivé(s) le : samedi 1 avril 2017 - 08:22:00

Fichier

jfla2013-13.pdf
Accord explicite pour ce dépôt

Identifiants

  • HAL Id : hal-00779903, version 1

Collections

Citation

Tom Gundersen, Willem Heijltjes, Michel Parigot. Un Lambda-Calcul Atomique. Damien Pous and Christine Tasson. JFLA - Journées francophones des langages applicatifs, Feb 2013, Aussois, France. 2013. 〈hal-00779903〉

Partager

Métriques

Consultations de la notice

249

Téléchargements de fichiers

116