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

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

Standard

Effectful Applicative Bisimilarity: Monads, Relators, and the Howe's Method. / Dal Lago, Ugo; Gavazzo, Francesco ; Levy, Paul Blain.

Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017). IEEE Computer Society Press, 2017. p. 1-12.

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

Harvard

Dal Lago, U, Gavazzo, F & Levy, PB 2017, Effectful Applicative Bisimilarity: Monads, Relators, and the Howe's Method. in Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017). IEEE Computer Society Press, pp. 1-12, 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017), Reykjavik, Iceland, 20/06/17. https://doi.org/10.1109/LICS.2017.8005117

APA

Dal Lago, U., Gavazzo, F., & Levy, P. B. (2017). Effectful Applicative Bisimilarity: Monads, Relators, and the Howe's Method. In Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017) (pp. 1-12). IEEE Computer Society Press. https://doi.org/10.1109/LICS.2017.8005117

Vancouver

Dal Lago U, Gavazzo F, Levy PB. Effectful Applicative Bisimilarity: Monads, Relators, and the Howe's Method. In Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017). IEEE Computer Society Press. 2017. p. 1-12 https://doi.org/10.1109/LICS.2017.8005117

Author

Dal Lago, Ugo ; Gavazzo, Francesco ; Levy, Paul Blain. / Effectful Applicative Bisimilarity: Monads, Relators, and the Howe's Method. Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017). IEEE Computer Society Press, 2017. pp. 1-12

Bibtex

@inproceedings{01e961eef53f42a098e70ac568125a46,
title = "Effectful Applicative Bisimilarity: Monads, Relators, and the Howe's Method",
abstract = "We study Abramsky{\textquoteright}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{\textquoteright}s method in the abstract. ",
author = "{Dal Lago}, Ugo and Francesco Gavazzo and Levy, {Paul Blain}",
year = "2017",
month = aug,
day = "18",
doi = "10.1109/LICS.2017.8005117",
language = "English",
pages = "1--12",
booktitle = "Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017)",
publisher = "IEEE Computer Society Press",
note = "32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017) ; Conference date: 20-06-2017 Through 23-06-2017",

}

RIS

TY - GEN

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

AU - Dal Lago, Ugo

AU - Gavazzo, Francesco

AU - Levy, Paul Blain

PY - 2017/8/18

Y1 - 2017/8/18

N2 - 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.

AB - 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.

U2 - 10.1109/LICS.2017.8005117

DO - 10.1109/LICS.2017.8005117

M3 - Conference contribution

SP - 1

EP - 12

BT - Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017)

PB - IEEE Computer Society Press

T2 - 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017)

Y2 - 20 June 2017 through 23 June 2017

ER -