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://hal.inria.fr/hal-01479035 https://hal.inria.fr/hal-01479035/document https://hal.inria.fr/hal-01479035/file/lics.pdf https://doi.org/10.1109/LICS.2017.8005118 |
id |
ftunivnantes:oai:HAL:hal-01479035v1 |
---|---|
record_format |
openpolar |
institution |
Open Polar |
collection |
Université de Nantes: HAL-UNIV-NANTES |
op_collection_id |
ftunivnantes |
language |
English |
topic |
Encoding Calculus Syntactics Semantics Magnetic heads Communication channels Interference [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] |
spellingShingle |
Encoding Calculus Syntactics Semantics Magnetic heads Communication channels Interference [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] Biernacka, Małgorzata Biernacki, Dariusz Lenglet, Sergueï Polesiuk, Piotr Pous, Damien Schmitt, Alan Fully Abstract Encodings of λ-Calculus in HOcore through Abstract Machines |
topic_facet |
Encoding Calculus Syntactics Semantics Magnetic heads Communication channels Interference [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] |
description |
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. |
author2 |
University of Wrocław Poland (UWr) Proof-oriented development of computer-based systems (MOSEL) Department of Formal Methods (LORIA - FM) Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA) Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA) Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS) Laboratoire de l'Informatique du Parallélisme (LIP) École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL) Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS) Preuves et Langages (PLUME) Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL) Software certification with semantic analysis (CELTIQUE) Inria Rennes – Bretagne Atlantique Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4) Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA) Université de Rennes 1 (UR1) Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées - Rennes (INSA Rennes) Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique) Institut Mines-Télécom Paris (IMT)-Institut Mines-Télécom Paris (IMT)-Université de Rennes 1 (UR1) Institut Mines-Télécom Paris (IMT)-Institut Mines-Télécom Paris (IMT)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA) Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique) Institut Mines-Télécom Paris (IMT)-Institut Mines-Télécom Paris (IMT) |
format |
Conference Object |
author |
Biernacka, Małgorzata Biernacki, Dariusz Lenglet, Sergueï Polesiuk, Piotr Pous, Damien Schmitt, Alan |
author_facet |
Biernacka, Małgorzata Biernacki, Dariusz Lenglet, Sergueï Polesiuk, Piotr Pous, Damien Schmitt, Alan |
author_sort |
Biernacka, Małgorzata |
title |
Fully Abstract Encodings of λ-Calculus in HOcore through Abstract Machines |
title_short |
Fully Abstract Encodings of λ-Calculus in HOcore through Abstract Machines |
title_full |
Fully Abstract Encodings of λ-Calculus in HOcore through Abstract Machines |
title_fullStr |
Fully Abstract Encodings of λ-Calculus in HOcore through Abstract Machines |
title_full_unstemmed |
Fully Abstract Encodings of λ-Calculus in HOcore through Abstract Machines |
title_sort |
fully abstract encodings of λ-calculus in hocore through abstract machines |
publisher |
HAL CCSD |
publishDate |
2017 |
url |
https://hal.inria.fr/hal-01479035 https://hal.inria.fr/hal-01479035/document https://hal.inria.fr/hal-01479035/file/lics.pdf https://doi.org/10.1109/LICS.2017.8005118 |
op_coverage |
Reykjavik, Iceland |
long_lat |
ENVELOPE(12.480,12.480,65.107,65.107) |
geographic |
Tive |
geographic_facet |
Tive |
genre |
Iceland |
genre_facet |
Iceland |
op_source |
LICS 2017 - 32nd Annual ACM/IEEE Symposium on Logic in Computer Science https://hal.inria.fr/hal-01479035 LICS 2017 - 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2017, Reykjavik, Iceland. ⟨10.1109/LICS.2017.8005118⟩ |
op_relation |
info:eu-repo/semantics/altIdentifier/doi/10.1109/LICS.2017.8005118 hal-01479035 https://hal.inria.fr/hal-01479035 https://hal.inria.fr/hal-01479035/document https://hal.inria.fr/hal-01479035/file/lics.pdf doi:10.1109/LICS.2017.8005118 |
op_rights |
info:eu-repo/semantics/OpenAccess |
op_doi |
https://doi.org/10.1109/LICS.2017.8005118 |
container_title |
2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) |
container_start_page |
1 |
op_container_end_page |
12 |
_version_ |
1766037904343171072 |
spelling |
ftunivnantes:oai:HAL:hal-01479035v1 2023-05-15T16:47:48+02:00 Fully Abstract Encodings of λ-Calculus in HOcore through Abstract Machines Biernacka, Małgorzata Biernacki, Dariusz Lenglet, Sergueï Polesiuk, Piotr Pous, Damien Schmitt, Alan University of Wrocław Poland (UWr) Proof-oriented development of computer-based systems (MOSEL) Department of Formal Methods (LORIA - FM) Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA) Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA) Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS) Laboratoire de l'Informatique du Parallélisme (LIP) École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL) Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS) Preuves et Langages (PLUME) Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL) Software certification with semantic analysis (CELTIQUE) Inria Rennes – Bretagne Atlantique Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4) Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA) Université de Rennes 1 (UR1) Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées - Rennes (INSA Rennes) Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique) Institut Mines-Télécom Paris (IMT)-Institut Mines-Télécom Paris (IMT)-Université de Rennes 1 (UR1) Institut Mines-Télécom Paris (IMT)-Institut Mines-Télécom Paris (IMT)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA) Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique) Institut Mines-Télécom Paris (IMT)-Institut Mines-Télécom Paris (IMT) Reykjavik, Iceland 2017-06 https://hal.inria.fr/hal-01479035 https://hal.inria.fr/hal-01479035/document https://hal.inria.fr/hal-01479035/file/lics.pdf https://doi.org/10.1109/LICS.2017.8005118 en eng HAL CCSD info:eu-repo/semantics/altIdentifier/doi/10.1109/LICS.2017.8005118 hal-01479035 https://hal.inria.fr/hal-01479035 https://hal.inria.fr/hal-01479035/document https://hal.inria.fr/hal-01479035/file/lics.pdf doi:10.1109/LICS.2017.8005118 info:eu-repo/semantics/OpenAccess LICS 2017 - 32nd Annual ACM/IEEE Symposium on Logic in Computer Science https://hal.inria.fr/hal-01479035 LICS 2017 - 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2017, Reykjavik, Iceland. ⟨10.1109/LICS.2017.8005118⟩ Encoding Calculus Syntactics Semantics Magnetic heads Communication channels Interference [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] info:eu-repo/semantics/conferenceObject Conference papers 2017 ftunivnantes https://doi.org/10.1109/LICS.2017.8005118 2023-03-01T05:56:25Z 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. Conference Object Iceland Université de Nantes: HAL-UNIV-NANTES Tive ENVELOPE(12.480,12.480,65.107,65.107) 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) 1 12 |