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. Some of my musings on the topic:
- Coming Soon: A Semantic Girard Translation for Dependent Type Theory with Applications to Coherence Spaces and Games.
- Samson Abramsky, Radha Jagadeesan, Matthijs Vákár, Game Semantics for Dependent Types. Journal paper. Under review.
- Samson Abramsky, Radha Jagadeesan, Matthijs Vákár, Games for Dependent Types. Proceedings of 42nd International Colloquium on Automata, Languages and Programming (ICALP 2015). Revised version on arXiv.
- Matthijs Vákár, Theory and Applications of Linear Dependent Types. Report for the transfer of status to DPhil candidate in the University of Oxford.
- Matthijs Vákár, Syntax and Semantics of Linear Dependent Types. Technical Report. ArXiv e-prints.
- Matthijs Vákár, A Categorical Semantics for Linear Logical Frameworks. Proceedings of Eighteenth International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2015).
- 28-07-2015 - Cork, Ireland, Domains XII - Game Semantics for Dependent Types (slides).
- 08-07-2015 - Kyoto, Japan, ICALP 2015 - Game Semantics for Dependent Types (slides).
- 04-06-2015 - Paris, France, Université Paris-Diderot (Paris 7), Laboratoire PPS, Séminaire PPS - Splitting the Atom of Dependent Types (slides).
- 13-04-2015 - London, UK, FoSSaCS 2015 - A Categorical Semantics for Linear Logical Frameworks (slides).
- 10-11-2014 - Oxford, UK, University of Oxford, QMAC Homotopy Type Theory Workshop - Splitting the Atom of Dependent Types (slides).
- 25-7-2014 - Birmingham, UK, University of Birmingham, Department of Computer Science, Theory Group Seminar - Syntax and Semantics of Linear Dependent Types (slides).
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.