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.
Dal Lago U., Gavazzo F., Tanaka R. (2020). Effectful applicative similarity for call-by-name lambda calculi. THEORETICAL COMPUTER SCIENCE, 813, 234-247 [10.1016/j.tcs.2019.12.025].
Effectful applicative similarity for call-by-name lambda calculi
Dal Lago U.
;Gavazzo F.;
2020
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.File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
main.pdf
accesso aperto
Tipo:
Postprint
Licenza:
Licenza per Accesso Aperto. Creative Commons Attribuzione - Non commerciale - Non opere derivate (CCBYNCND)
Dimensione
1.39 MB
Formato
Adobe PDF
|
1.39 MB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
