Sound and Complete Bisimilarities for Call-by-Name and Call-by-Value Lambda-mu Calculus

Abstract : We propose the first sound and complete bisimilarities for the call-by-name and call-by-value untyped lambda-mu calculus. We define applicative bisimilarities for both semantics and environmental bisimilarity for call-by-name. We give equivalence examples to illustrate how our relations can be used; in particular, we prove David and Py's counter-example, which cannot be proved with Lassen's preexisting normal form bisimilarities for the lambda-mu calculus.
Liste complète des métadonnées

Cited literature [20 references]  Display  Hide  Download

https://hal.inria.fr/hal-00926100
Contributor : Sergueï Lenglet <>
Submitted on : Wednesday, July 30, 2014 - 11:45:38 AM
Last modification on : Tuesday, December 18, 2018 - 4:38:25 PM
Document(s) archivé(s) le : Tuesday, November 25, 2014 - 9:00:35 PM

File

RR-8447.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00926100, version 2

Citation

Dariusz Biernacki, Sergueï Lenglet. Sound and Complete Bisimilarities for Call-by-Name and Call-by-Value Lambda-mu Calculus. [Research Report] RR-8447, INRIA. 2014. ⟨hal-00926100v2⟩

Share

Metrics

Record views

580

Files downloads

495