Skip to Main content Skip to Navigation
Journal articles

Effectful applicative similarity for call-by-name lambda calculi

Ugo Dal Lago 1, 2 Francesco Gavazzo 3, 2 Ryo Tanaka 4
2 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
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.
Document type :
Journal articles
Complete list of metadatas

Cited literature [29 references]  Display  Hide  Download

https://hal.inria.fr/hal-02991694
Contributor : Francesco Gavazzo <>
Submitted on : Friday, November 6, 2020 - 10:04:01 AM
Last modification on : Saturday, November 7, 2020 - 3:35:51 AM

File

mainExtended.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Ugo Dal Lago, Francesco Gavazzo, Ryo Tanaka. Effectful applicative similarity for call-by-name lambda calculi. Theoretical Computer Science, Elsevier, 2020, 813, pp.234-247. ⟨10.1016/j.tcs.2019.12.025⟩. ⟨hal-02991694⟩

Share

Metrics

Record views

9

Files downloads

38