Effectful Applicative Bisimilarity: Monads, Relators, and Howe's Method
International audience We study Abramsky's applicative bisimilarity abstractly , in the context of call-by-value λ-calculi with algebraic effects. We first of all endow a computational λ-calculus with a monadic operational semantics. We then show how the theory of relators provides precisely wh...
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-01636365 https://inria.hal.science/hal-01636365/document https://inria.hal.science/hal-01636365/file/lics2017HAL.pdf https://doi.org/10.1109/LICS.2017.8005117 |
id |
ftunivcotedazur:oai:HAL:hal-01636365v1 |
---|---|
record_format |
openpolar |
spelling |
ftunivcotedazur:oai:HAL:hal-01636365v1 2024-01-14T10:07:56+01:00 Effectful Applicative Bisimilarity: Monads, Relators, and Howe's Method Dal Lago, Ugo Gavazzo, Francesco Blain Levy, Paul Alma Mater Studiorum Università di Bologna = University of Bologna (UNIBO) Foundations of Component-based Ubiquitous Systems (FOCUS) Inria Sophia Antipolis - Méditerranée (CRISAM) Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria) School of Computer Science Birmingham University of Birmingham Birmingham ANR-16-CE25-0011,REPAS,Des systèmes logiciels fiables et conscients des données privées, via les métriques de bisimulation(2016) Reykjavik, Iceland 2017-06-20 https://inria.hal.science/hal-01636365 https://inria.hal.science/hal-01636365/document https://inria.hal.science/hal-01636365/file/lics2017HAL.pdf https://doi.org/10.1109/LICS.2017.8005117 en eng HAL CCSD IEEE info:eu-repo/semantics/altIdentifier/doi/10.1109/LICS.2017.8005117 hal-01636365 https://inria.hal.science/hal-01636365 https://inria.hal.science/hal-01636365/document https://inria.hal.science/hal-01636365/file/lics2017HAL.pdf doi:10.1109/LICS.2017.8005117 info:eu-repo/semantics/OpenAccess Logic in Computer Science (LICS), 2017 32nd Annual ACM/IEEE Symposium on LICS 2017 - ACM/IEEE Symposium on Logic in Computer Science https://inria.hal.science/hal-01636365 LICS 2017 - ACM/IEEE Symposium on Logic in Computer Science, Jun 2017, Reykjavik, Iceland. pp.1-12, ⟨10.1109/LICS.2017.8005117⟩ ACM: D.: Software/D.3: PROGRAMMING LANGUAGES/D.3.1: Formal Definitions and Theory/D.3.1.0: Semantics [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] info:eu-repo/semantics/conferenceObject Conference papers 2017 ftunivcotedazur https://doi.org/10.1109/LICS.2017.8005117 2023-12-19T23:45:34Z International audience We study Abramsky's applicative bisimilarity abstractly , in the context of call-by-value λ-calculi with algebraic effects. We first of all endow a computational λ-calculus with a monadic operational semantics. We then show how the theory of relators provides precisely what is needed to generalise applicative bisimilarity to such a calculus, and to single out those monads and relators for which applicative bisimilarity is a congruence, thus a sound methodology for program equivalence. This is done by studying Howe's method in the abstract. Conference Object Iceland HAL Université Côte d'Azur 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) 1 12 |
institution |
Open Polar |
collection |
HAL Université Côte d'Azur |
op_collection_id |
ftunivcotedazur |
language |
English |
topic |
ACM: D.: Software/D.3: PROGRAMMING LANGUAGES/D.3.1: Formal Definitions and Theory/D.3.1.0: Semantics [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] |
spellingShingle |
ACM: D.: Software/D.3: PROGRAMMING LANGUAGES/D.3.1: Formal Definitions and Theory/D.3.1.0: Semantics [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] Dal Lago, Ugo Gavazzo, Francesco Blain Levy, Paul Effectful Applicative Bisimilarity: Monads, Relators, and Howe's Method |
topic_facet |
ACM: D.: Software/D.3: PROGRAMMING LANGUAGES/D.3.1: Formal Definitions and Theory/D.3.1.0: Semantics [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] |
description |
International audience We study Abramsky's applicative bisimilarity abstractly , in the context of call-by-value λ-calculi with algebraic effects. We first of all endow a computational λ-calculus with a monadic operational semantics. We then show how the theory of relators provides precisely what is needed to generalise applicative bisimilarity to such a calculus, and to single out those monads and relators for which applicative bisimilarity is a congruence, thus a sound methodology for program equivalence. This is done by studying Howe's method in the abstract. |
author2 |
Alma Mater Studiorum Università di Bologna = University of Bologna (UNIBO) Foundations of Component-based Ubiquitous Systems (FOCUS) Inria Sophia Antipolis - Méditerranée (CRISAM) Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria) School of Computer Science Birmingham University of Birmingham Birmingham ANR-16-CE25-0011,REPAS,Des systèmes logiciels fiables et conscients des données privées, via les métriques de bisimulation(2016) |
format |
Conference Object |
author |
Dal Lago, Ugo Gavazzo, Francesco Blain Levy, Paul |
author_facet |
Dal Lago, Ugo Gavazzo, Francesco Blain Levy, Paul |
author_sort |
Dal Lago, Ugo |
title |
Effectful Applicative Bisimilarity: Monads, Relators, and Howe's Method |
title_short |
Effectful Applicative Bisimilarity: Monads, Relators, and Howe's Method |
title_full |
Effectful Applicative Bisimilarity: Monads, Relators, and Howe's Method |
title_fullStr |
Effectful Applicative Bisimilarity: Monads, Relators, and Howe's Method |
title_full_unstemmed |
Effectful Applicative Bisimilarity: Monads, Relators, and Howe's Method |
title_sort |
effectful applicative bisimilarity: monads, relators, and howe's method |
publisher |
HAL CCSD |
publishDate |
2017 |
url |
https://inria.hal.science/hal-01636365 https://inria.hal.science/hal-01636365/document https://inria.hal.science/hal-01636365/file/lics2017HAL.pdf https://doi.org/10.1109/LICS.2017.8005117 |
op_coverage |
Reykjavik, Iceland |
genre |
Iceland |
genre_facet |
Iceland |
op_source |
Logic in Computer Science (LICS), 2017 32nd Annual ACM/IEEE Symposium on LICS 2017 - ACM/IEEE Symposium on Logic in Computer Science https://inria.hal.science/hal-01636365 LICS 2017 - ACM/IEEE Symposium on Logic in Computer Science, Jun 2017, Reykjavik, Iceland. pp.1-12, ⟨10.1109/LICS.2017.8005117⟩ |
op_relation |
info:eu-repo/semantics/altIdentifier/doi/10.1109/LICS.2017.8005117 hal-01636365 https://inria.hal.science/hal-01636365 https://inria.hal.science/hal-01636365/document https://inria.hal.science/hal-01636365/file/lics2017HAL.pdf doi:10.1109/LICS.2017.8005117 |
op_rights |
info:eu-repo/semantics/OpenAccess |
op_doi |
https://doi.org/10.1109/LICS.2017.8005117 |
container_title |
2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) |
container_start_page |
1 |
op_container_end_page |
12 |
_version_ |
1788062343368802304 |