Lawvere - Tierney sheaves in Algebraic Set Theory. - Steven Awodey; Nicola Gambino; Peter LeFanu Lumsdaine; Michael A. Warren (J. Symb. Log., 2009)

Weak omega-categories from intensional type theory - Peter LeFanu Lumsdaine (Log. Methods Comput. Sci., 2010)

Quipper: a scalable quantum programming language. - Alexander S. Green; Peter LeFanu Lumsdaine; Neil J. Ross; Peter Selinger; Benoît Valiron (PLDI, 2013)

An Introduction to Quantum Programming in Quipper. - Alexander S. Green; Peter LeFanu Lumsdaine; Neil J. Ross; Peter Selinger; Benoît Valiron (RC, 2013)

Homotopy limits in Coq - Jeremy Avigad; Krzysztof Kapulkin; Peter LeFanu Lumsdaine (CoRR, 2013)

Homotopy limits in type theory. - Jeremy Avigad; Krzysztof Kapulkin; Peter LeFanu Lumsdaine (Math. Struct. Comput. Sci., 2015)

The Local Universes Model: An Overlooked Coherence Construction for Dependent Type Theories. - Peter LeFanu Lumsdaine; Michael A. Warren (ACM Trans. Comput. Log., 2015)

A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory. - Kuen-Bang Hou (Favonia); Eric Finster; Daniel R. Licata; Peter LeFanu Lumsdaine (LICS, 2016)

Parametricity, Automorphisms of the Universe, and Excluded Middle. - Auke Bart Booij; Martín Hötzel Escardó; Peter LeFanu Lumsdaine; Michael Shulman (TYPES, 2016)

The HoTT library: a formalization of homotopy type theory in Coq. - Andrej Bauer; Jason Gross; Peter LeFanu Lumsdaine; Michael Shulman; Matthieu Sozeau; Bas Spitters (CPP, 2017)

Formalization of Mathematics in Type Theory (Dagstuhl Seminar 18341). - Andrej Bauer; Martín Hötzel Escardó; Peter LeFanu Lumsdaine; Assia Mahboubi (Dagstuhl Reports, 2018)

Categorical structures for type theory in univalent foundations. - Benedikt Ahrens; Peter LeFanu Lumsdaine; Vladimir Voevodsky (Log. Methods Comput. Sci., 2018)

Preface: Special Issue on Homotopy Type Theory and Univalent Foundations. - Peter LeFanu Lumsdaine; Nicolas Tabareau (J. Autom. Reason., 2019)

Constructive reflectivity Principles for Regular Theories. - Henrik Forssell; Peter LeFanu Lumsdaine (J. Symb. Log., 2019)

Displayed Categories. - Benedikt Ahrens; Peter LeFanu Lumsdaine (Log. Methods Comput. Sci., 2019)

A general definition of dependent type theories. - Andrej Bauer; Philipp G. Haselwarter; Peter LeFanu Lumsdaine (CoRR, 2020)

Special issue on homotopy type theory 2019. - Dan Licata; Peter LeFanu Lumsdaine (Math. Struct. Comput. Sci., 2021)

Special issue on homotopy type theory 2019 vol. 2. - Dan Licata; Peter LeFanu Lumsdaine (Math. Struct. Comput. Sci., 2023)

Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories. - Benedikt Ahrens; Peter LeFanu Lumsdaine; Paige Randall North (APLAS, 2024)