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 [22 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01650000
Contributeur : Sergueï Lenglet <>
Soumis le : mardi 28 novembre 2017 - 10:32:10
Dernière modification le : jeudi 11 janvier 2018 - 06:25:24

Fichier

mfps.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01650000, version 1

Citation

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〉

Partager

Métriques

Consultations de la notice

74

Téléchargements de fichiers

28