Supervisors

Suitable for

Abstract

Prerequisites: Some knowledge of programming language semantics

Background

 

The semantics of the λ-calculus has been studied for a long time, and this research slowly uncovered some connections with the theory of algebraic structures. This perspective was finally made clear by Hyland [1], who gives an algebraic perspective on the λ-calculus, inspired by some concepts from category theory, and shows that this perspective can be used to show some of the most important theorems of the λ-calculus. There has been less work on the π-calculus, which is a model of computation designed around concurrent processes.

Focus

 

This project aims to take the first steps towards an algebraic perspective on the π-calculus, similar to the work that has been done for the λ-calculus. The main goal would be to develop a notion of π-theory analogous to Hyland's notion of λ-theory, and to study their basic properties. Extensions could involve using this notion of π-theory to prove important results about the π-calculus.

 

Method

 

The starting point would be Stark's work on models of π-calculus [2]. The notion of π-theory should be an adaptation of the notion of model described by Stark. Once you have a proposed definition, you will be able to start proving some basic properties about it, which would justify that it really is a good notion of π-theory.

 

[1] Martin Hyland, Classical lambda calculus in modern dress. Mathematical Structures in Computer Science, 2015.

[2] Ian Stark. Free-algebra models for the π-calculus. Theoretical Computer Science, 2008.