HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Effectful Normal Form Bisimulation

Ugo Dal Lago 1, 2 Francesco Gavazzo 2, 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 : Normal form bisimulation, also known as open bisimulation, is a coinductive technique for higher-order program equivalence in which programs are compared by looking at their essentially infinitary tree-like normal forms, i.e. at their Böhm or Lévy-Longo trees. The technique has been shown to be useful not only when proving metatheorems about λ-calculi and their semantics, but also when looking at concrete examples of terms. In this paper, we show that there is a way to generalise normal form bisimulation to calculi with algebraic effects, à la Plotkin and Power. We show that some mild conditions on monads and relators, which have already been shown to guarantee effectful applicative bisimi-larity to be a congruence relation, are enough to prove that the obtained notion of bisimilarity, which we call effectful normal form bisimilarity, is a congruence relation, and thus sound for contextual equivalence. Additionally , contrary to applicative bisimilarity, normal form bisimilarity allows for enhancements of the bisimulation proof method, hence proving a powerful reasoning principle for effectful programming languages.
Document type :
Conference papers
Complete list of metadata

Cited literature [73 references]  Display  Hide  Download

https://hal.inria.fr/hal-02386004
Contributor : Francesco Gavazzo Connect in order to contact the contributor
Submitted on : Friday, November 29, 2019 - 10:29:47 AM
Last modification on : Wednesday, February 2, 2022 - 3:56:14 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02386004, version 1

Collections

Citation

Ugo Dal Lago, Francesco Gavazzo. Effectful Normal Form Bisimulation. ESOP 2019 - European Symposium on Programming, Apr 2019, Prague, Czech Republic. ⟨hal-02386004⟩

Share

Metrics

Record views

82

Files downloads

112