References & Citations
Computer Science > Logic in Computer Science
Title: Fully Abstract Encodings of $λ$-Calculus in HOcore through Abstract Machines
(Submitted on 13 May 2022 (v1), last revised 12 Apr 2023 (this version, v3))
Abstract: We present fully abstract encodings of the call-by-name and call-by-value $\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 of the encodings. We also demonstrate that this technique scales to the $\lambda\mu$-calculus, i.e., a standard extension of the $\lambda$-calculus with control operators.
Submission history
From: Sergueï Lenglet [view email][v1] Fri, 13 May 2022 14:16:22 GMT (54kb)
[v2] Mon, 16 May 2022 14:04:55 GMT (54kb)
[v3] Wed, 12 Apr 2023 14:44:26 GMT (61kb)
Link back to: arXiv, form interface, contact.