Fully Abstract Encodings of λ-Calculus in HOcore through Abstract Machines
International audience 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 equival...
Published in: | 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) |
---|---|
Main Authors: | , , , , , |
Other Authors: | , , , , , , , , , , , , , , , , , , , , |
Format: | Conference Object |
Language: | English |
Published: |
HAL CCSD
2017
|
Subjects: | |
Online Access: | https://inria.hal.science/hal-01479035 https://inria.hal.science/hal-01479035/document https://inria.hal.science/hal-01479035/file/lics.pdf https://doi.org/10.1109/LICS.2017.8005118 |
Summary: | International audience 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. |
---|