Menu:
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
-
Homotopical inverse diagrams in categories with attributes, Krzysztof Kapulkin and Peter LeFanu Lumsdaine. Submitted. arXiv:1808.01816
-
Semantics of higher inductive types, Peter LeFanu Lumsdaine and Michael Shulman. To appear in Mathematical Proceedings of the Cambridge Philosophical Society, 2020. doi:10.1017/S030500411900015X; arXiv:1705.07088
-
The simplicial model of univalent foundations (after Voevodsky), Krzysztof Kapulkin and Peter LeFanu Lumsdaine. To appear in Journal of the European Mathematical Society, 2020. arXiv:1211.2851
-
Constructive reflection principles for regular theories, Henrik Forssell and Peter LeFanu Lumsdaine. To appear in Journal of Symbolic Logic, 2020. arXiv:1604.03851 doi:10.1017/jsl.2019.70
-
Displayed categories, Benedikt Ahrens and Peter LeFanu Lumsdaine. Logical Methods in Computer Science, Vol. 15, March 2019. doi:10.23638/LMCS-15(1:20)2019; arXiv:1705.04296
Conference version: 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), ed. D. Michael Miller, LIPIcs 84. doi:10.4230/LIPIcs.FSCD.2017.5; arXiv:1705.04296v2
-
The homotopy theory of type theories, Krzysztof Kapulkin and Peter LeFanu Lumsdaine. Advances in Mathematics 337, 2018. doi:10.1016/j.aim.2018.08.003; arXiv:1610.00037
-
Categorical structures for type theory in univalent foundations, Benedikt Ahrens, Peter LeFanu Lumsdaine, and Vladimir Voevodsky. Logical Methods in Computer Science, Vol 14(3), September 2018. doi:10.23638/LMCS-14(3:18)2018; arXiv:1705.04310
Conference version: 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), Ed. Valentin Goranko and Mads Dam. LIPIcs 82. doi:10.4230/LIPIcs.CSL.2017.8; arXiv:1705.04310
-
Parametricity, automorphisms of the universe, and excluded middle, Auke Bart Booij, Martín Hötzel Escardó, Peter LeFanu Lumsdaine, and Michael Shulman. Post-proceedings of TYPES 2016, LPIPcs 97, ed. Silvia Ghilezan, Herman Geuvers, and Jelena Ivetić. doi:10.4230/LIPIcs.TYPES.2016.7; arXiv:1701.05617
-
The HoTT Library: A formalization of homotopy type theory in Coq, A. Bauer, J. Gross, P. LeF. Lumsdaine, M. Shulman, M. Sozeau, and B. Spitters. In Proceedings of CPP 2017, ed. Yves Bertot and Viktor Vafeiadis, Association for Computing Machinery, 2017. doi:10.1145/3018610.3018615; arXiv:1610.04591
-
A mechanization of the Blakers–Massey connectivity theorem in homotopy type theory, Kuen-Bang Hou (Favonia), Eric Finster, Dan R. Licata, and Peter LeFanu Lumsdaine. Proceedings of LICS ’16. doi:10.1145/2933575.2934545; arXiv:1605.03227
-
The local universes model: an overlooked coherence construction for dependent type theories, Peter LeFanu Lumsdaine and Michael A. Warren. ACM Transactions on Computational Logic 16.3, 2015. doi:10.1145/2754931; arXiv:1411.1736
-
Homotopy limits in type theory, Jeremy Avigad, Krzysztof Kapulkin, and Peter LeFanu Lumsdaine. Mathematical Structures in Computer Science 25(5), 2015. doi:10.1017/S0960129514000498; arXiv:1304.0680
-
Quipper: A scalable quantum programming language, A. S. Green, P. LeF. Lumsdaine, N. J. Ross, P. Selinger, and B. Valiron. SIGPLAN Notices 48(6), June 2013. doi:10.1145/2499370.2462177; arXiv:1304.3390
-
An introduction to quantum programming in Quipper, A. S. Green, Peter LeFanu Lumsdaine, N. J. Ross, P. Selinger, and B. Valiron. In Reversible Computation, 2013, ed. Gerhard W. Dueck and D. Michael Miller. Springer LNCS 7948. doi:10.1007/978-3-642-38986-3_10; arXiv:1304.5485
-
On the Bourbaki–Witt principle in toposes, Andrej Bauer and Peter LeFanu Lumsdaine. Mathematical Proceedings of the Cambridge Philosophical Society 155, July 2013. doi:10.1017/S0305004113000108; arXiv:1201.0340
-
Homotopy type theory: Univalent foundations of mathematics (The HoTT Book), The Univalent Foundations Program (many-author collaboration), 2013. Homepage
-
Univalence in Simplicial Sets, Krzysztof Kapulkin, Peter LeFanu Lumsdaine, and Vladimir Voevodsky. Unpublished note, 2012. arXiv:1203.2553
-
Model Structures from Higher Inductive Types, Peter LeFanu Lumsdaine. Unpublished note, December 2011. pdf
-
A small observation on co-categories, Peter LeFanu Lumsdaine. Theory and Applications of Categories 25(9), 2011. arXiv:0902.4743; journal page
-
Higher Categories from Type Theories (PhD thesis), Peter LeFanu Lumsdaine. Carnegie Mellon University, 2010. pdf
-
Weak ω-categories from intensional type theory, Peter LeFanu Lumsdaine. Logical Methods in Computer Science 6(3), 2010. doi:10.2168/LMCS-6(3:24)2010; arXiv:0812.0409v4
Conference version: Typed Lambda Calculi and Applications 2009, Springer LNCS 5608. doi:10.1007/978-3-642-02273-9_14
-
Lawvere–Tierney sheaves in Algebraic Set Theory, Steve Awodey, Nicola Gambino, Peter LeFanu Lumsdaine, and Michael A. Warren. Journal of Symbolic Logic 74.3, September 2009. doi:10.2178/jsl/1245158088; arXiv:0711.1529
Selected talks
-
December 2018, Formalising the initiality conjecture in Coq and Agda. Joint talk with Guillaume Brunerie, at Stockholm–Göteborg Type Theory Serminar — slides (pdf) (PLL’s sections only)
-
August 2017, A general (syntactic) definition of dependent type theories. Logic Colloquium 2017, Stockholm, secret special session on type theory (organised by Erik Palmgren) — slides
-
May 2016, Homotopy-theoretic models of type theory. Mini-course at Fields Institute workshop on HoTT/UF — abstract and video
-
June 2011, 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)