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 λ-calculus into HOcore, a minimal higher-order process calculus with no name restriction. We consider several equivalences on the λ-calculus side—normal-form bisimilarity, applica-tive bisimilarity, and contextual equivalence—that we internalize into abstract machines in order to prove full abstraction.
Document type :
Conference papers
Complete list of metadatas

Contributor : Sergueï Lenglet <>
Submitted on : Tuesday, February 28, 2017 - 3:47:32 PM
Last modification on : Friday, September 13, 2019 - 9:48:42 AM
Long-term archiving on : Monday, May 29, 2017 - 3:39:26 PM


Files produced by the author(s)



Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk, Damien Pous, et al.. Fully Abstract Encodings of λ-Calculus in HOcore through Abstract Machines. LICS 2017, Jun 2017, Reykjavik, Iceland. ⟨10.1109/LICS.2017.8005118⟩. ⟨hal-01479035⟩



Record views


Files downloads