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 fullabstraction result for such a generic, coinductive methodology for program equivalence.
Titolo: | Effectful applicative similarity for call-by-name lambda calculi | |
Autore/i: | Lago, Ugo Dal; Gavazzo, Francesco; Tanaka, Ryo | |
Autore/i Unibo: | ||
Anno: | 2017 | |
Titolo del libro: | Joint Proceedings of the 18th Italian Conference on Theoretical Computer Science and the 32nd Italian Conference on Computational Logic co-located with the 2017 IEEE International Workshop on Measurements and Networking 2017 IEEE M&N | |
Pagina iniziale: | 87 | |
Pagina finale: | 98 | |
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 fullabstraction result for such a generic, coinductive methodology for program equivalence. | |
Data stato definitivo: | 7-feb-2018 | |
Appare nelle tipologie: | 4.01 Contributo in Atti di convegno |
File in questo prodotto:
Eventuali allegati, non sono esposti
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.