Effectful Applicative Bisimilarity: Monads, Relators, and Howe's Method (Long Version)

2017/04/15 by Lago, Ugo Dal, Gavazzo, Francesco, Levy, Paul Blain · 1 citation
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Programming Languages (cs.PL)

paper · doi:10.48550/arxiv.1704.04647

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.

Cited by

• Higher-Order Behavioural Conformances via Fibrations

Related

• Applicative Bisimulation and Quantum λ-Calculi (Long Version)
• Applicative Bisimulations for Delimited-Control Operators
• A more general categorical framework for congruence of applicative bisimilarity
• Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances (Extended Version)
• On Probabilistic Applicative Bisimulation and Call-by-Value\n \λ-Calculi (Long Version)