- Typed behavioural equivalences in the Pi-Calculus
- Prebet, Enguerrand <1996>
Description
- 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.
Date
- 2022-09-27
Type
- Doctoral Thesis
- PeerReviewed
Format
- application/pdf
Identifier
urn:nbn:it:unibo-29026
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