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


https://hal.inria.fr/hal-01507625
Contributeur : Sergueï Lenglet <>
Soumis le : jeudi 13 avril 2017 - 14:31:19
Dernière modification le : mercredi 2 août 2017 - 10:07:07

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

252

Téléchargements du document

36