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...

Full description

Bibliographic Details
Published in:2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
Main Authors: Dal Lago, Ugo, Gavazzo, Francesco, Blain Levy, Paul
Other Authors: Alma Mater Studiorum Università di Bologna 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)-Dipartimento di Informatica - Scienza e Ingegneria Bologna (DISI), Alma Mater Studiorum Università di Bologna Bologna (UNIBO)-Alma Mater Studiorum Università di Bologna Bologna (UNIBO), 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
Language:English
Published: HAL CCSD 2017
Subjects:
Online Access:https://hal.inria.fr/hal-01636365
https://hal.inria.fr/hal-01636365/document
https://hal.inria.fr/hal-01636365/file/lics2017HAL.pdf
https://doi.org/10.1109/LICS.2017.8005117
Description
Summary: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.