Peter LeFanu Lumsdaine
Peter LeFanu Lumsdaine
Postdoctoral researcher, Mathematics, Stockholm University
Verified email at math.su.se - Homepage
TitleCited byYear
Quipper: a scalable quantum programming language
AS Green, PLF Lumsdaine, NJ Ross, P Selinger, B Valiron
ACM SIGPLAN Notices 48 (6), 333-342, 2013
2062013
The simplicial model of univalent foundations (after Voevodsky)
C Kapulkin, PLF Lumsdaine
arXiv preprint arXiv:1211.2851, 2012
1872012
Weak omega-categories from intensional type theory
PLF Lumsdaine
1072008
Semantics of higher inductive types
PLF Lumsdaine, M Shulman
Mathematical Proceedings of the Cambridge Philosophical Society, 1-50, 2017
56*2017
An introduction to quantum programming in quipper
AS Green, PLF Lumsdaine, NJ Ross, P Selinger, B Valiron
International Conference on Reversible Computation, 110-124, 2013
522013
The local universes model: an overlooked coherence construction for dependent type theories
PLF Lumsdaine, MA Warren
ACM Transactions on Computational Logic (TOCL) 16 (3), 23, 2015
51*2015
The HoTT library: a formalization of homotopy type theory in Coq
A Bauer, J Gross, PLF Lumsdaine, M Shulman, M Sozeau, B Spitters
Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and …, 2017
432017
Homotopy limits in Coq
J Avigad, K Kapulkin, PLF Lumsdaine
arXiv preprint arXiv:1304.0680, 4, 2013
31*2013
Higher inductive types: a tour of the menagerie
PLF Lumsdaine
URl: http://homotopytypetheory. org/2011/04/24/higher-induc tive-types-a …, 2011
212011
Univalence in simplicial sets
C Kapulkin, PLF Lumsdaine, V Voevodsky
arXiv preprint arXiv:1203.2553, 2012
182012
Higher Categories from Type Theories (CT2011, Vancouver)
PLF Lumsdaine
16*2010
Model structures from higher inductive types
PL Lumsdaine
Unpublished note, December, 2011
122011
The homotopy theory of type theories
K Kapulkin, PLF Lumsdaine
Advances in Mathematics 337, 1-38, 2018
72018
Categorical structures for type theory in univalent foundations
B Ahrens, PLF Lumsdaine, V Voevodsky
arXiv preprint arXiv:1705.04310, 2017
72017
A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory
KB Hou, E Finster, D Licata, PLF Lumsdaine
arXiv preprint arXiv:1605.03227, 2016
7*2016
Lawvere–Tierney sheaves in algebraic set theory
S Awodey, N Gambino, PL Lumsdaine, MA Warren
The Journal of Symbolic Logic 74 (3), 861-890, 2009
72009
Displayed Categories
B Ahrens, PLF Lumsdaine
arXiv preprint arXiv:1705.04296, 2017
52017
Parametricity, automorphisms of the universe, and excluded middle
AB Booij, MH Escardó, PLF Lumsdaine, M Shulman
arXiv preprint arXiv:1701.05617, 2017
42017
On the Bourbaki–Witt principle in toposes
A Bauer, PL Lumsdaine
Mathematical Proceedings of the Cambridge Philosophical Society 155 (1), 87-99, 2013
42013
A Coq proof that Univalence Axioms implies Functional Extensionality
A Bauer, PLF Lumsdaine
32011
The system can't perform the operation now. Try again later.
Articles 1–20