Categorical proof theory

There is a strong connection between programs and the proofs for certain logics. By finding mathematical models for either of these we increase our understanding of them. Because logical connectives relate closely to constructions in the model it is often mathematically cleaner to consider the former. (Categorical) proof theory is concerned with how proofs may be modelled, and which proofs can be considered equivalent to each other. While there are some logics whose proof theory is well understood these are fairly limited. The aim of this project is to extend what is known to more interesting logics, or to find more adaptable models (based on specific criteria for desirable properties).