Effectful applicative similarity for call-by-name lambda calculi - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Theoretical Computer Science Année : 2020

Effectful applicative similarity for call-by-name lambda calculi

Résumé

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
mainExtended.pdf (486.89 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02991694 , version 1 (06-11-2020)

Identifiants

Citer

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

Altmetric

Partager

Gmail Facebook X LinkedIn More