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.
Type de document :
Communication dans un congrès
ICTCS 2017 - 18th Italian Conference on Theoretical Computer Science, Sep 2017, Naples, Italy
Liste complète des métadonnées

Littérature citée [20 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01636368
Contributeur : Francesco Gavazzo <>
Soumis le : jeudi 16 novembre 2017 - 15:11:51
Dernière modification le : samedi 27 janvier 2018 - 01:31:38
Document(s) archivé(s) le : samedi 17 février 2018 - 15:12:02

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

69

Téléchargements de fichiers

19