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