Effectful applicative similarity for call-by-name lambda calculi - Archive ouverte HAL Access content directly
Conference Papers Year :

Effectful applicative similarity for call-by-name lambda calculi

(1, 2) , (2, 3) , (4)
1
2
3
4

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.
Fichier principal
Vignette du fichier
main.pdf (471.18 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01636368 , version 1 (16-11-2017)

Identifiers

  • HAL Id : hal-01636368 , version 1

Cite

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⟩
90 View
94 Download

Share

Gmail Facebook Twitter LinkedIn More