Effectful applicative similarity for call-by-name lambda calculi

Abstract : We introduce a notion of applicative similarity in which not terms but monadic values arising from the evaluation of effectful terms, can be compared. We prove this notion to be fully abstract whenever terms are evaluated in call-by-name order. This is the first full-abstraction result for such a generic, coinductive methodology for program equivalence.
Complete list of metadatas

Cited literature [20 references]  Display  Hide  Download

https://hal.inria.fr/hal-01636368
Contributor : Francesco Gavazzo <>
Submitted on : Thursday, November 16, 2017 - 3:11:51 PM
Last modification on : Saturday, September 29, 2018 - 1:15:34 AM
Long-term archiving on : Saturday, February 17, 2018 - 3:12:02 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01636368, version 1

Collections

Citation

Ugo Dal Lago, Francesco Gavazzo, Ryo Tanaka. Effectful applicative similarity for call-by-name lambda calculi. ICTCS 2017 - 18th Italian Conference on Theoretical Computer Science, Sep 2017, Naples, Italy. ⟨hal-01636368⟩

Share

Metrics

Record views

146

Files downloads

62