At the moment, I am mostly spending my time trying to map the landscape of type theories (in the broad sense of the word) and their categorical semantics. Of special interest to me are intuitive semantic presentations of initial - or fully abstract/complete, in CS terms - models of syntactic calculi. The two approaches that spring to mind, in particular, are the constructions of these models either as categories of games and strategies or as categories of geometric objects like (generalised) tangles. I'm hoping that a good understanding of this "big picture" will help relate diverse concepts coming from fields like computer science, physics, geometry (homotopy theory), logic, and linguistics, through the comparison of categories and type theories coming from these areas.
More concretely, my main project, at the moment, is an investigation into linear dependent type theory and its semantics. This research programme consists of a few parts, which are at various stages of completion, with many being in the queue for a detailed writeup. If you are interested in any of the topics below, please don't hesitate to drop me a line for some discussion! Preprints available on request.
- Developing a general theory of the syntax and semantics of linear dependent types: technical report, paper published in proceedings of FoSSaCS 2015.
- Explaining the Girard translation of intuitionistic dependent type theory into the linear variant, from a semantic point of view: see upcoming paper.
- Extending the coherence space model of propositional linear type theory to dependent types: see upcoming paper with Samson Abramsky.
- Building a model in terms of AJM-games, hence providing a game semantics for dependent types: see upcoming paper with Radha Jagadeesan and Samson Abramsky.
- Providing an account of the initial model, in terms of tangles, extending string diagrams to linear dependent types: planned.
- Studying a model in stable homotopy theory and investigating its connections with HoTT: planned.
- Studying models related to quantum physics: planned.
An outline of my research programme is given in my first year report.
Master's thesis on topos-theoretic approaches to quantum kinematics, a survey article of the field, unifying some of the definitions and results and presenting some new ones.
Bachelor's thesis on principal bundles and gauge theory, a set of lecture notes that was intended to form an addition to the then existing literature by connecting the mathematical and physical parts of the story.