On the categorical semantics of homotopy type theory in simplicial sets/-groupoids:
On higher inductive types in homotopy type theory:
Peter LeFanu Lumsdaine, Higher inductive types, a tour of the menagerie (2011) [blog post]
Peter LeFanu Lumsdaine, Higher Inductive Types: The circle and friends, axiomatically (2011) [pdf, pdf]
and on their categorical semantics:
with precursors in:
Mike Shulman, Peter LeFanu Lumsdaine, Semantics of higher inductive types (2012) [pdf]
Mike Shulman, Peter LeFanu Lumsdaine, Semantics and syntax of higher inductive types (2016) [slides]
On synthetic homotopy theory in homotopy type theory:
Introducing the functional quantum programming language Quipper:
Alexander Green, Peter LeFanu Lumsdaine, Neil Ross, Peter Selinger, Benoît Valiron, Quipper: A Scalable Quantum Programming Language, ACM SIGPLAN Notices 48(6):333-342, 2013 (arXiv:1304.3390)
Alexander Green, Peter LeFanu Lumsdaine, Neil Ross, Peter Selinger, Benoît Valiron, An Introduction to Quantum Programming in Quipper, Lecture Notes in Computer Science 7948:110-124, Springer, 2013 (arXiv:1304.5485)
On the categorical semantics of dependent type theory via comprehension categories:
Formalization of (the proof of) the Blakers-Massey theorem in homotopy type theory:
Last revised on February 14, 2023 at 15:14:15. See the history of this page for a list of all contributions to it.