Coinductive Equivalences and Metrics for Higher-order Languages with Algebraic Effects

Gavazzo, Francesco (2019) Coinductive Equivalences and Metrics for Higher-order Languages with Algebraic Effects, [Dissertation thesis], Alma Mater Studiorum Università di Bologna. Dottorato di ricerca in Computer science and engineering, 31 Ciclo. DOI 10.6092/unibo/amsdottorato/9075.
Documenti full-text disponibili:
[img] Documento PDF (English) - Richiede un lettore di PDF come Xpdf o Adobe Acrobat Reader
Disponibile con Licenza: Creative Commons Attribution Non-commercial Share Alike 3.0 (CC BY-NC-SA 3.0) .
Download (1MB)


This dissertation investigates notions of program equivalence and metric for higher-order sequential languages with algebraic effects. Computational effects are those aspects of computation that involve forms of interaction with the environment. Due to such an interactive behaviour, reasoning about effectful programs is well-known to be hard. This is especially true for higher-order effectful languages, where programs can be passed as input to, and returned as output by other programs, as well as perform side-effects. Additionally, when dealing with effectful languages, program equivalence is oftentimes too coarse, not allowing, for instance, to quantify the observable differences between programs. A natural way to overcome this problem is to re ne the notion of a program equivalence into the one of a program distance or program metric, this way allowing for a finer, quantitative analysis of program behaviour. A proper account of program distance, however, requires a more sophisticated theory than program equivalence, both conceptually and mathematically. This often makes the study of program distance way more di cult than the corresponding study of program equivalence.

Tipologia del documento
Tesi di dottorato
Gavazzo, Francesco
Dottorato di ricerca
Settore disciplinare
Settore concorsuale
Parole chiave
bisimulation coinduction lambda calculus
Data di discussione
3 Aprile 2019

Altri metadati

Statistica sui download

Gestione del documento: Visualizza la tesi