Fully Abstract Encodings of $\lambda$-Calculus in HOcore through Abstract Machines

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

Publikováno v: Logical Methods in Computer Science, Vol Volume 20, Issue 3 (2024)

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

Externí odkaz: https://doaj.org/article/893fc1f102a24a21a8a9597b6d1f848e

Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation

Autor: Andrés Aristizábal, Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk

Publikováno v: Logical Methods in Computer Science, Vol Volume 13, Issue 3 (2017)

We present sound and complete environmental bisimilarities for a variant of Dybvig et al.'s calculus of multi-prompted delimited-control operators with dynamic prompt generation. The reasoning principles that we obtain generalize and advance the exis

Externí odkaz: https://doaj.org/article/40b0d2a723cf4dca87cf606c6cce6a6e

Certified Derivation of Small-Step From Big-Step Skeletal Semantics

Autor: Guillaume Ambal, Sergueï Lenglet, Alan Schmitt, Camille NoûS

Publikováno v: PPDP 2022-24th International Symposium on Principles and Practice of Declarative Programming
PPDP 2022-24th International Symposium on Principles and Practice of Declarative Programming, Sep 2022, Tbilisi, Georgia. pp.1-48, ⟨10.1145/3551357.3551384⟩

International audience; We present an automatic translation of a skeletal semantics written in big-step style into an equivalent structural operational semantics. This translation is implemented on top of the Necro tool, which lets us automatically g

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::0ac4e4d406c5e66ce1991dd5a1ca48e1
https://inria.hal.science/hal-03768820

Diacritical Companions

Autor: Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk

Publikováno v: MFPS 2019-Mathematical Foundations of Programming Semantics XXXV
MFPS 2019-Mathematical Foundations of Programming Semantics XXXV, Jun 2019, London, United Kingdom. ⟨10.1016/j.entcs.2019.09.003⟩

International audience; Coinductive reasoning in terms of bisimulations is in practice routinely supported by carefully crafted up-to techniques that can greatly simplify proofs. However, designing and proving such bisimulation enhancements sound can

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::96efbc5e7258d179846543f3b9ddf66a
https://inria.hal.science/hal-02136002

Proving Soundness of Extensional Normal-Form Bisimilarities

Autor: Sergueï Lenglet, Piotr Polesiuk, Dariusz Biernacki

Publikováno v: Mathematical Foundations of Programming Semantics XXXIII
Mathematical Foundations of Programming Semantics XXXIII, Jun 2017, Ljubljana, Slovenia. ⟨10.1016/j.entcs.2018.03.015⟩
Logical Methods in Computer Science
Logical Methods in Computer Science, 2019, 15 (1), pp.31:1-31:24. ⟨10.23638/LMCS-15(1:31)2019⟩
MFPS
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2019, 15 (1), pp.31:1-31:24. ⟨10.23638/LMCS-15(1:31)2019⟩

International audience; Normal-form bisimilarity is a simple, easy-to-use behavioral equivalence that relates terms in lambda-calculi by decomposing their normal forms into bisimilar subterms. Moreover, it typically allows for powerful up-to techniqu

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::2de32c0e725c970d2513b66ca9e225a1
https://hal.inria.fr/hal-01650000