Fully Abstract Encodings of λ-Calculus in HOcore through Abstract Machines

Résumé : Nous présentons des encodages complètement abstraits du lambda-calcul en appel par nom en HOcore, un calcul d’ordre supérieur minimal, sans restriction de noms. Nous considérons plusieurs équivalences du côté du lambda-calcul—les bisimilarités de forme normale et applicative, et l’équivalence contextuelle—que nous internalisons dans des machines abstraites pour prouver l’abstraction complète.
Type de document :
Rapport
[Research Report] RR-9052, Inria. 2017
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01507625
Contributeur : Sergueï Lenglet <>
Soumis le : jeudi 13 avril 2017 - 14:31:19
Dernière modification le : mercredi 16 mai 2018 - 11:24:13

Fichier

RR-9052.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01507625, version 1

Citation

Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk, Damien Pous, et al.. Fully Abstract Encodings of λ-Calculus in HOcore through Abstract Machines. [Research Report] RR-9052, Inria. 2017. 〈hal-01507625〉

Partager

Métriques

Consultations de la notice

645

Téléchargements de fichiers

95