Skip to Main content Skip to Navigation

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

Małgorzata Biernacka 1 Dariusz Biernacki 1 Sergueï Lenglet 2 Piotr Polesiuk 1 Damien Pous 3, 4 Alan Schmitt 5
2 PAREO - Formal islands: foundations and applications
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
4 PLUME - Preuves et Langages
LIP - Laboratoire de l'Informatique du Parallélisme
5 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : 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.
Document type :
Complete list of metadatas

Cited literature [23 references]  Display  Hide  Download
Contributor : Sergueï Lenglet <>
Submitted on : Thursday, April 13, 2017 - 2:31:19 PM
Last modification on : Saturday, July 11, 2020 - 3:15:19 AM


Files produced by the author(s)


  • HAL Id : hal-01507625, version 1


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⟩



Record views


Files downloads