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
Contributor : Francesco Gavazzo <>
Submitted on : Friday, November 29, 2019 - 10:29:47 AM
Last modification on : Friday, October 30, 2020 - 12:04:04 PM


Files produced by the author(s)


  • HAL Id : hal-02386004, version 1



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



Record views


Files downloads