My research lies broadly in category theory, logic, and constructive mathematics. Most of my recent work is within or related to the Homotopy Type Theory/Univalent Foundations programme: developing dependent type theory as a foundation for mathematics, drawing on ideas from homotopy theory and higher category theory.
I am also interested in quantum programming languages (I worked on the early stages of Quipper) and mathematical computing.
Publications & preprints
 The homotopy theory of type theories, with Chris Kapulkin, preprint (2016). pdf · arXiv
 The HoTT Library: A formalization of homotopy type theory in Coq, with Bauer, Gross, Shulman, Sozeau, and Spitters, submitted (2016). pdf · arXiv
 Constructive reflection principles for regular theories, with Henrik Forssell, submitted (2016). pdf · arXiv
 A mechanization of the Blakers–Massey connectivity theorem in homotopy type theory, with KuenBang Hou, Eric Finster, and Dan Licata, Logic in Computer Science (LICS 2016), to appear.
 The local universes model: an overlooked coherence construction for dependent type theories, with Michael A. Warren, ACM Trans. Computational Logic 16, no. 3, pp.23.1–23.31 (2014). pdf · arXiv · journal
 Homotopy limits in type theory, with Jeremy Avigad and Chris Kapulkin, Mathematical Structures in Computer Science, 25(05), pp.1040–1070 (2014). pdf · arXiv · journal
 The simplicial model of Univalent Foundations, with Chris Kapulkin and Vladimir Voevodsky, preprint (2014). arXiv Shorter version (simplicial aspects only): Univalence in Simplicial Sets (2012). arXiv
 Homotopy Type Theory: Univalent Foundations of Mathematics, “The HoTT book”, collaborative book by the Univalent Foundations Group (2013). website
 Quipper: A Scalable Quantum Programming Language, with Alexander Green, Julien Ross, Peter Selinger, and Benoît Valiron, ACM SIGPLAN Notices 48(6):333342 (2013). arXiv
 An introduction to Quantum Programming in Quipper, with Alexander Green, Julien Ross, Peter Selinger, and Benoît Valiron, for RC2013, Lecture Notes in Computer Science 7948:110124, Springer (2013). arXiv
 Model Structures from Higher Inductive Types. Proves that any type theory with HIT’s (sepcifically, mapping cylinder types) admits most of the structure of a model category. Unpublished note (2011). pdf
 On the BourbakiWitt Principle in Toposes, with Andrej Bauer, Mathematical Proceedings of the Cambridge Philosophical Society, Vol. 155, No. 1 (2012). A miscellany of constructive proofs and countermodels, on the theme of the BourbakiWitt fixedpoint theorem. pdf · arXiv · journal
 A Small Observation on Cocategories, Theory and Applications of Categories, Vol. 25, No. 9, pp.247–250 (2011). “Every cocategory in a coherent category is a coequivalence relation.” Short note, four pages (2008). pdf · arXiv · journal
 PhD thesis: Higher Categories from Type Theories, Carnegie Mellon University (2010). pdf
 Weak ωCategories from Intensional Type Theory. Originally presented at TLCA 2009,
Brasília; journal version in Logical Methods in Computer Science, Vol. 6, issue 23, paper 24 (2010). pdf · arXiv · journal · proceedings
 LawvereTierney Sheaves in Algebraic Set Theory, with Steve Awodey, Nicola Gambino and Michael A. Warren, Journal of Symbolic Logic, Vol. 74, Issue 3, pp.861–890 (2009). pdf · arXiv
Talks

Formalising the semantics of DTT, in DTT,
DMV 2015, Hamburg, September 2015.
Slides: pdf

Higher Categories from Dependent Type Theories, CT2011, Vancouver, July 2011. An overview of part of my thesis work. (Taught me an important lesson in proofreading: start at the title slide, not the beginning of the text. Thanks to those who pointed this out after my talk, having decided that Higer was the squirrel at the end.) Slides: pdf

Homotopy Type Theory: a very short introduction, OPLSS, Eugene, June 2011. Does what it says on the tin. Slides: pdf

Higher Inductive Types: the circle and friends, axiomatically, FMCS 2011, Kananaskis, Alberta. An overview of homotopy type theory, and an introduction to higher inductive types, with pictures. Slides: pdf

Conservativity principles: a homotopytheoretic approach, Octoberfest 2010, Halifax. An elementary demonstration of how techniques from Homotopy Theory can be profitably applied in Type Theory. This was for a semispecialsession, so is a little lighter on DTT background than it might have been otherwise. Slides: pdf

Topology and Algebra: an introduction to duality, CMU Grad Seminar, April 2009. Expository talk, for a general mathematical audience: presenting Gel’fand Duality, as a jumpingoff point to illustrate the ideas of noncommutative geometry/topology and the language of category theory. Slides: pdf

Weak ωcategories and intensional type theory, October 2008. Handwritten notes from talks in CMU logic seminar. Not at first intended for public comsumption; quality improves as they go on. Talks 1–3 are entirely expository, 1 on type theory, 2 and 3 and the start of 4 on Tom Leinster's definition of weak ωcategories.
Talk 1 (Extremely scrappy notes.) A quick introduction to Intensional ML Type Theory.
Talk 2 Strict higher categories, and operads, in preparation for weak higher categories.
Talk 3 Globular operads, in preparation for weak higher categories.
Talk 4 Finally: weak higher categories! and a construction of the "fundamental weak ωcategory" of a type.