My doctoral project is a theoretical investigation into dependent type theory. Dependent types form the basis for programming logics like Coq and Agda, which may be used to formalise logical reasoning and, in particular, give formal proofs about the correctness of computer programs. As it stands, only so-called pure dependently typed languages are well understood, in which crucial practical programming constructs like printing, recursion, mutable state, control operators, non-determinism and probabilistic choice are excluded. My DPhil contributes towards a better understanding of the possibilities of extending dependent types towards more realistic impure languages. This analysis has so far been performed by looking at dependent types from the points of view of linear logic, game semantics and call-by-push-value.
Recently, I have been working on probabilistic programming with Neil Dhir. Specifically, we are modelling lion behaviour using Bayesian non-parametrics.
Some of my musings:
- Coming Soon: A Semantic Girard Translation for Dependent Type Theory with Applications to Information Systems, Coherence Spaces and Games.
- An Effectful Treatment of Dependent Types. Under review.
- A Framework for Dependent Types and Effects. ArXiv e-prints.
- Game Semantics for Dependent Types. With Samson Abramsky and Radha Jagadeesan. Accepted for publication in Information and Computation.
- Games for Dependent Types. With Samson Abramsky and Radha Jagadeesan. Proceedings of 42nd International Colloquium on Automata, Languages and Programming (ICALP 2015). Revised version on arXiv.
- Theory and Applications of Linear Dependent Types. Report for the transfer of status to DPhil candidate in the University of Oxford.
- Syntax and Semantics of Linear Dependent Types. Technical Report. ArXiv e-prints.
- A Categorical Semantics for Linear Logical Frameworks. Proceedings of Eighteenth International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2015).
- 05-04-2017 - New York, US, Center for Data Science, New York University - An Intro to Curry-Howard and Verification: Relating Logic and Machine Learning (slides).
- 03-04-2016 - Eindhoven, Netherlands, GaLoP 2016 - Effectful Game Semantics for Dependent Types (slides).
- 20-10-2015 - Bath, UK, Department of Computer Science, Mathematical Foundations Seminar - Game Semantics for Dependent Types [Extended Version] (slides).
- 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.