Follow
Peter LeFanu Lumsdaine
Peter LeFanu Lumsdaine
Assistant professor, Dept. of Mathematics, Stockholm University
Verified email at math.su.se - Homepage
Title
Cited by
Cited by
Year
Quipper: a scalable quantum programming language
AS Green, PLF Lumsdaine, NJ Ross, P Selinger, B Valiron
Proceedings of the 34th ACM SIGPLAN conference on Programming language …, 2013
3962013
The simplicial model of univalent foundations (after Voevodsky)
C Kapulkin, PLF Lumsdaine
Journal of the European Mathematical Society, to appear; preprint arXiv:1211 …, 2012
297*2012
Weak omega-categories from intensional type theory
PLF Lumsdaine
1322008
Homotopy type theory: Univalent foundations of mathematics
TUFP (collaboration)
Institute for Advanced Study (Princeton), The Univalent Foundations Program …, 2013
114*2013
Semantics of higher inductive types
PLF Lumsdaine, M Shulman
Mathematical Proceedings of the Cambridge Philosophical Society 169 (1), 159-208, 2020
112*2020
The local universes model: an overlooked coherence construction for dependent type theories
PLF Lumsdaine, MA Warren
ACM Transactions on Computational Logic (TOCL) 16 (3), 1-31, 2015
892015
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
842017
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
772013
Homotopy limits in Coq
J Avigad, K Kapulkin, PLF Lumsdaine
arXiv preprint arXiv:1304.0680 4, 2013
45*2013
The homotopy theory of type theories
K Kapulkin, PLF Lumsdaine
Advances in Mathematics 337, 1-38, 2018
332018
Displayed categories
B Ahrens, PLF Lumsdaine
arXiv preprint arXiv:1705.04296, 2017
302017
A mechanization of the Blakers–Massey connectivity theorem in homotopy type theory
KBH Favonia, E Finster, DR Licata, PLF Lumsdaine
2016 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1-10, 2016
27*2016
Higher inductive types: a tour of the menagerie
PLF Lumsdaine
242011
Categorical structures for type theory in univalent foundations
B Ahrens, PLF Lumsdaine, V Voevodsky
arXiv preprint arXiv:1705.04310, 2017
232017
Univalence in simplicial sets
C Kapulkin, PLF Lumsdaine, V Voevodsky
arXiv:1203.2553, 2012
212012
Higher Categories from Type Theories (PhD thesis)
PLF Lumsdaine
Carnegie Mellon University, 2010
192010
Model structures from higher inductive types
PLF Lumsdaine
url: http://peterlefanulumsdaine.com/research/Lumsdaine-Model-strux-from …, 2011
122011
A general definition of dependent type theories
A Bauer, PG Haselwarter, PLF Lumsdaine
arXiv preprint arXiv:2009.05539, 2020
102020
Lawvere–Tierney sheaves in Algebraic Set Theory
S Awodey, N Gambino, PL Lumsdaine, MA Warren
Journal of Symbolic Logic 74 (3), 861-890, 2009
10*2009
Parametricity, automorphisms of the universe, and excluded middle
AB Booij, MH Escardó, PLF Lumsdaine, M Shulman
arXiv preprint arXiv:1701.05617, 2017
92017
The system can't perform the operation now. Try again later.
Articles 1–20