Project of the Applied Category Theory Adjoint School 2020
Mentor: Valeria de Paiva
TA: Jade Edenstar Master
Project description
Dialectica categories (also called dialectica spaces) were introduced in the doctoral work of de Paiva [1], where they were used to model Gödel’s dialectica interpretation [2], as well as to provide categorical models of Girard’s linear logic [3]. Since then several applications of dialectica categories, have been described. We want to have some more of them.
This project is about categories of Petri nets. The goal is to update and develop the work started by Carolyn Brown and Doug Gurr in [4] and further pursued in [5] and [6]. Neither of the latter two have been officially published, but they have had some impact on the concurrency community, as shown by their number of citations. It seems sensible to see whether the work on Petri nets and concurrency has proved or disproved the original suggestions.
Petri nets are an extremely popular model of concurrency, both in theory and in practice. They have several descriptions and variations in the literature. One of the interesting problems with Petri nets was to give a compositional theory of them. Brown and Gurr used dialectica categories to model a restricted class of Petri nets in [4]. They were joined by de Paiva in [5], which generalized the previous work to nets of multiplicity greater than one. The mathematical basis was described in [6]. Their nets have morphisms corresponding to simulations, which we believe are more flexible than the ones usually considered.
References
- V. de Paiva, The Dialectica Categories. Phd Thesis, University of Cambridge, UK, 1990.
- K. Gödel, About an as yet unmentioned extension of the finite point of view. Dialectica 12, 280-297, 1958.
- J. Y. Girard, Linear logic. Theoretical Computer Science 50, 1-101, 1987.
- C. Brown and D. Gurr, A categorical linear framework for Petri nets. Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science, 208-218, 1990.
- C. Brown, D. Gurr and V. de Paiva, A linear specification language for Petri nets. Aarhus technical report, 1991.
- V. de Paiva, Categorical multirelations, linear logic and Petri nets. Technical report, 1991.
The selected readings for the presentations will be [4] and [6].