This project aims to investigate the application of proof-theoretic techniques to problems in the operational semantics of true (non- interleaving) concurrency. The research will explore a fruitful relationship between Petri nets and linear logic theories which gives rise to a correspondence between net token games and linear proof trees. This correspondence makes it possible to see that algorithms and theorems from the proof theory of linear logic can be applied to problems in net theory and, conversely, that results about nets have consequences for provability in fragments of linear logic. For example, standard proof-theoretic concepts such as cut elimination give rise to algorithms for increasing the concurrency in an execution sequence on a net. On the other hand, the decidability of forward markings on nets can be used to show decidability for a significant collection of linear logic formulas. Concepts such as the interpretation of logical theories and conservative extension may be useful in understanding abstraction for nets. Moreover, it is hoped that this idea for understanding concurrency in proof trees will lead to the discovery of other interesting models of concurrency.
