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
Liste complète des métadonnées

https://hal.inria.fr/hal-01479035
Contributor : Sergueï Lenglet <>
Submitted on : Tuesday, February 28, 2017 - 3:47:32 PM
Last modification on : Wednesday, February 20, 2019 - 2:32:07 PM
Document(s) archivé(s) le : Monday, May 29, 2017 - 3:39:26 PM

File

lics.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01479035, 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. LICS 2017, Jun 2017, Reykjavik, Iceland. ⟨hal-01479035⟩

Share

Metrics

Record views

1366

Files downloads

117