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

Ugo Dal Lago 1, 2 Francesco Gavazzo 1, 2 Paul Blain Levy 3
2 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [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.
Type de document :
Communication dans un congrès
LICS 2017 - ACM/IEEE Symposium on Logic in Computer Science, Jun 2017, Reykjavik, Iceland. IEEE, Logic in Computer Science (LICS), 2017 32nd Annual ACM/IEEE Symposium on, pp.1-12, 〈10.1109/LICS.2017.8005117〉
Liste complète des métadonnées

Littérature citée [39 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01636365
Contributeur : Francesco Gavazzo <>
Soumis le : mardi 5 décembre 2017 - 14:47:13
Dernière modification le : samedi 27 janvier 2018 - 01:31:48

Identifiants

Collections

Citation

Ugo Dal Lago, Francesco Gavazzo, Paul Blain Levy. Effectful Applicative Bisimilarity: Monads, Relators, and Howe's Method. LICS 2017 - ACM/IEEE Symposium on Logic in Computer Science, Jun 2017, Reykjavik, Iceland. IEEE, Logic in Computer Science (LICS), 2017 32nd Annual ACM/IEEE Symposium on, pp.1-12, 〈10.1109/LICS.2017.8005117〉. 〈hal-01636365〉

Partager

Métriques

Consultations de la notice

54

Téléchargements de fichiers

25