Skip to Main content Skip to Navigation
Conference papers

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

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 metadata

https://hal.inria.fr/hal-01479035
Contributor : Sergueï Lenglet <>
Submitted on : Tuesday, February 28, 2017 - 3:47:32 PM
Last modification on : Saturday, September 11, 2021 - 3:18:33 AM
Long-term archiving on: : Monday, May 29, 2017 - 3:39:26 PM

File

lics.pdf
Files produced by the author(s)

Identifiers

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 - 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2017, Reykjavik, Iceland. ⟨10.1109/LICS.2017.8005118⟩. ⟨hal-01479035⟩

Share

Metrics

Record views

1681

Files downloads

552