Małgorzata Biernacka ; Dariusz Biernacki ; Sergueï Lenglet ; Piotr Polesiuk ; Damien Pous et al. - Fully Abstract Encodings of $\lambda$-Calculus in HOcore through Abstract Machines

lmcs:9565 - Logical Methods in Computer Science, July 3, 2024, Volume 20, Issue 3 - https://doi.org/10.46298/lmcs-20(3:3)2024
Fully Abstract Encodings of $\lambda$-Calculus in HOcore through Abstract MachinesArticle

Authors: Małgorzata Biernacka ; Dariusz Biernacki ; Sergueï Lenglet ; Piotr Polesiuk ; Damien Pous ; Alan Schmitt

    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.


    Volume: Volume 20, Issue 3
    Published on: July 3, 2024
    Accepted on: May 1, 2024
    Submitted on: May 17, 2022
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 1180 times.
    This article's PDF has been downloaded 543 times.