Effectful applicative bisimilarity: monads, relators, and the Howe's method

Ugo Dal Lago; Francesco  Gavazzo; Paul Blain Levy

doi:10.1109/LICS.2017.8005117

Effectful applicative bisimilarity: monads, relators, and the Howe's method

Ugo Dal Lago, Francesco Gavazzo, Paul Blain Levy

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

12 Citations (Scopus)

241 Downloads (Pure)

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	https://doi.org/10.1109/LICS.2017.8005117
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

Access to Document

10.1109/LICS.2017.8005117

Effectful Applicative Bisimilarity
(c) 2017 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other users, including reprinting/ republishing this material for advertising or promotional purposes, creating new collective works for resale or redistribution to servers or lists, or reuse of any copyrighted components of this work in other works. Eligibility for repository: Checked on 5/5/2017
Accepted author manuscript, 433 KBLicence: None: All rights reserved

Cite this

@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",

isbn = "9781509030194",

pages = "1--12",

booktitle = "2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)",

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",

}

Dal Lago, U, Gavazzo, F & Levy, PB 2017, Effectful applicative bisimilarity: monads, relators, and the Howe's method. in 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). 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

TY - GEN

T1 - Effectful applicative bisimilarity

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

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

SN - 9781509030194

SP - 1

EP - 12

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

PB - IEEE Computer Society Press

Y2 - 20 June 2017 through 23 June 2017

ER -

Effectful applicative bisimilarity: monads, relators, and the Howe's method

Abstract

Conference

Access to Document

Fingerprint

Cite this