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.
Effectful applicative bisimilarity: Monads, relators, and Howe's method / Dal Lago, Ugo; Gavazzo, Francesco; Levy, Paul Blain. - ELETTRONICO. - (2017), pp. 1-12. (Intervento presentato al convegno 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017 tenutosi a Reykjavik, Iceland nel 2017) [10.1109/LICS.2017.8005117].
Effectful applicative bisimilarity: Monads, relators, and Howe's method
Dal Lago, Ugo
;GAVAZZO, FRANCESCO
;
2017
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
