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.
Original language | English |
---|---|
Title of host publication | 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) |
Publisher | IEEE Computer Society Press |
Pages | 1-12 |
Number of pages | 30 |
ISBN (Electronic) | 9781509030187 |
ISBN (Print) | 9781509030194 |
DOIs | |
Publication status | Published - 18 Aug 2017 |
Event | 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017) - Reykjavik, Iceland Duration: 20 Jun 2017 → 23 Jun 2017 |
Conference
Conference | 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017) |
---|---|
Country/Territory | Iceland |
City | Reykjavik |
Period | 20/06/17 → 23/06/17 |