Applicative Bisimilarities for Call-by-Name and Call-by-Value λμ-Calculus

Dariusz Biernacki 1 Sergueï Lenglet 2
1 Faculty of Mathematics and Computer Science [Wroclaw]
2 PAREO - Formal islands: foundations and applications
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : We propose the first sound and complete bisimilarities for the call-by-name and call-by-value untyped λµ-calculus, defined in the applicative style. 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 λµ-calculus.
Keywords : control operator continuation applicative bisimulation contextual equivalence
Document type :
Conference papers
Complete list of metadatas

Cited literature [19 references]  Display  Hide  Download
https://hal.inria.fr/hal-01080960
Contributor : Sergueï Lenglet <>
Submitted on : Thursday, November 6, 2014 - 3:33:17 PM
Last modification on : Friday, April 12, 2019 - 10:20:07 AM
Long-term archiving on : Saturday, February 7, 2015 - 11:06:29 AM

File

lambdamuentcs.pdf
Files produced by the author(s)

Identifiers

Collections

INRIA | UNIV-LORRAINE | LORIA-FM | LORIA

Citation

Dariusz Biernacki, Sergueï Lenglet. Applicative Bisimilarities for Call-by-Name and Call-by-Value λμ-Calculus. Mathematical Foundations of Programming Semantics Thirtieth Conference, Jun 2014, Ithaca, United States. pp.49 - 64, ⟨10.1016/j.entcs.2014.10.004⟩. ⟨hal-01080960⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

202

Files downloads

291

Contact


archive-ouverte@inria.fr