Effectful Applicative Bisimilarity: Monads, Relators, and the Howe's Method

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Authors

Colleges, School and Institutes

External organisations

  • University of Bologna

Abstract

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.

Details

Original languageEnglish
Title of host publicationProceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017)
Publication statusPublished - 18 Aug 2017
Event32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017) - Reykjavik, Iceland
Duration: 20 Jun 201723 Jun 2017

Conference

Conference32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017)
CountryIceland
CityReykjavik
Period20/06/1723/06/17