Typed behavioural equivalences in the Pi-Calculus

Prebet, Enguerrand (2022) Typed behavioural equivalences in the Pi-Calculus, [Dissertation thesis], Alma Mater Studiorum Università di Bologna. Dottorato di ricerca in Computer science and engineering, 36 Ciclo. DOI 10.48676/unibo/amsdottorato/10520.
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 No Derivatives 4.0 (CC BY-NC-ND 4.0) .
Download (1MB)


In this thesis, I study the notion of program equivalences, i.e. proving that two programs can be used interchangeably without altering the overall observable behaviour. This definition is highly dependent on the contexts in which these programs can be used; does the context have exceptions, parallelism, etc... So proofs also need to be adapted according to the expressiveness of those contexts. This thesis presents on the pi-calculus – a concurrent programming language – under various typing constraints. Types allows us to impose different disciplines like forcing a sequential execution, or ensuring linearity, meaning an object can be used once. In each case, the bisimulation, a standard proof technique for the pi-calculus, needs to be adapted accordingly to obtain a suitable equivalence. We then test how using the modified bisimulations can be used to reason about a language with higher-order functions and references, which once translated into the pi-calculus satisfies the typing constraints.

Tipologia del documento
Tesi di dottorato
Prebet, Enguerrand
Dottorato di ricerca
Settore concorsuale
Parole chiave
Formal proofs, Programming languages, Behavioural equivalences, Process calculi, Encodings, Bisimulation
Data di discussione
27 Settembre 2022

Altri metadati

Statistica sui download

Gestione del documento: Visualizza la tesi