Concurrency and Linear Logic

Alex Kavvos

To this day we have not managed to identify a unifying, fundamental mathematical structure behind concurrency theory and concurrent programming. This project is about re-visiting the idea of whether a formal system known as Linear Logic, which has recently been used as a system of session types, can be used as a basis for concurrent programming. The project involves work on the syntax of (idealised) concurrent programming languages, the categorical semantics of linear logic, as well as investigations on the relationship between these two. The project can be adapted to a student’s background, which can be in either Computer Science or Mathematics.