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

Encodages complètement abstraits du λ en HOcore à l’aide de machines abstraites

Małgorzata Biernacka (1) , Dariusz Biernacki (1) , Sergueï Lenglet (2) , Piotr Polesiuk (1) , Damien Pous (3, 4) , Alan Schmitt (5)

1 UWr - University of Wrocław [Poland]
2 MOSEL - Proof-oriented development of computer-based systems
3 LIP - Laboratoire de l'Informatique du Parallélisme
4 PLUME - Preuves et Langages
5 CELTIQUE - Software certification with semantic analysis

We present fully abstract encodings of the call-by-name lambda-calculus into HOcore, a minimal higher-order process calculus with no name restriction. We consider several equivalences on the lambda-calculus side---normal-form bisimilarity, applicative bisimilarity, and contextual equivalence---that we internalize into abstract machines in order to prove full abstraction.

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.

Mots clés: abstract machines; process calculi; higher-order; lambda-calculus

Mots clés: machines abstraites; ordre supérieur; lambda-calcul; calculs de processus

Domaines: Langage de programmation [cs.PL]

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⟩