Proving Soundness of Extensional Normal-Form Bisimilarities

Abstract : Normal-form bisimilarity is a simple, easy-to-use behavioral equivalence that relates terms in λ-calculi by decomposing their normal forms into bisimilar subterms. Besides, they allow for powerful up-to techniques, such as bisimulation up to context, which simplify bisimulation proofs even further. However, proving soundness of these relations becomes complicated in the presence of η-expansion and usually relies on ad-hoc proof methods which depend on the language. In this paper, we propose a more systematic proof method to show that an extensional normal-form bisimilarity along with its corresponding bisimulation up to context are sound. We illustrate our technique with the call-by-value λ-calculus, before applying it to a call-by-value λ-calculus with the delimited-control operators shift and reset. In both cases, there was previously no sound bisimulation up to context validating the η-law. Our results have been formalized in the Coq proof assistant.
Type de document :
Communication dans un congrès
Mathematical Foundations of Programming Semantics XXXIII, Jun 2017, Ljubljana, Slovenia
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger
Contributeur : Sergueï Lenglet <>
Soumis le : mardi 28 novembre 2017 - 10:32:10
Dernière modification le : jeudi 11 janvier 2018 - 06:25:24


Fichiers produits par l'(les) auteur(s)


  • HAL Id : hal-01650000, version 1



Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk. Proving Soundness of Extensional Normal-Form Bisimilarities. Mathematical Foundations of Programming Semantics XXXIII, Jun 2017, Ljubljana, Slovenia. 〈hal-01650000〉



Consultations de la notice


Téléchargements de fichiers