Peter LeFanu Lumsdaine

Publication Activity (10 Years)

Years Active: 2009-2021
Publications (10 Years): 18

Top Topics

Theoretical Framework

Top Venues

Math. Struct. Comput. Sci.

Log. Methods Comput. Sci.

Publications

Dan Licata, Peter LeFanu Lumsdaine
Special issue on homotopy type theory 2019. Math. Struct. Comput. Sci. 31 (10) (2021)
Andrej Bauer, Philipp G. Haselwarter, Peter LeFanu Lumsdaine
A general definition of dependent type theories. CoRR (2020)
Henrik Forssell, Peter LeFanu Lumsdaine
Constructive reflectivity Principles for Regular Theories. J. Symb. Log. 84 (4) (2019)
Benedikt Ahrens, Peter LeFanu Lumsdaine
Displayed Categories. Log. Methods Comput. Sci. 15 (1) (2019)
Peter LeFanu Lumsdaine, Nicolas Tabareau
Preface: Special Issue on Homotopy Type Theory and Univalent Foundations. J. Autom. Reason. 63 (2) (2019)
Benedikt Ahrens, Peter LeFanu Lumsdaine, Vladimir Voevodsky
Categorical structures for type theory in univalent foundations. Log. Methods Comput. Sci. 14 (3) (2018)
Andrej Bauer, Martín Hötzel Escardó, Peter LeFanu Lumsdaine, Assia Mahboubi
Formalization of Mathematics in Type Theory (Dagstuhl Seminar 18341). Dagstuhl Reports 8 (8) (2018)
Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, Bas Spitters
The HoTT library: a formalization of homotopy type theory in Coq. CPP (2017)
Benedikt Ahrens, Peter LeFanu Lumsdaine, Vladimir Voevodsky
Categorical Structures for Type Theory in Univalent Foundations. CSL (2017)
Benedikt Ahrens, Peter LeFanu Lumsdaine
Displayed Categories. FSCD (2017)
Auke Bart Booij, Martín Hötzel Escardó, Peter LeFanu Lumsdaine, Michael Shulman
Parametricity, automorphisms of the universe, and excluded middle. CoRR (2017)
Benedikt Ahrens, Peter LeFanu Lumsdaine, Vladimir Voevodsky
Categorical structures for type theory in univalent foundations. CoRR (2017)
Auke Bart Booij, Martín Hötzel Escardó, Peter LeFanu Lumsdaine, Michael Shulman
Parametricity, Automorphisms of the Universe, and Excluded Middle. TYPES (2016)
Kuen-Bang Hou, Eric Finster, Daniel R. Licata, Peter LeFanu Lumsdaine
A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory. CoRR (2016)
Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, Bas Spitters
The HoTT Library: A formalization of homotopy type theory in Coq. CoRR (2016)
Kuen-Bang Hou (Favonia), Eric Finster, Daniel R. Licata, Peter LeFanu Lumsdaine
A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory. LICS (2016)
Peter LeFanu Lumsdaine, Michael A. Warren
The Local Universes Model: An Overlooked Coherence Construction for Dependent Type Theories. ACM Trans. Comput. Log. 16 (3) (2015)
Jeremy Avigad, Krzysztof Kapulkin, Peter LeFanu Lumsdaine
Homotopy limits in type theory. Math. Struct. Comput. Sci. 25 (5) (2015)
Jeremy Avigad, Krzysztof Kapulkin, Peter LeFanu Lumsdaine
Homotopy limits in Coq CoRR (2013)
Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, Benoît Valiron
An Introduction to Quantum Programming in Quipper CoRR (2013)
Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, Benoît Valiron
Quipper: a scalable quantum programming language. PLDI (2013)
Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, Benoît Valiron
Quipper: A Scalable Quantum Programming Language CoRR (2013)
Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, Benoît Valiron
An Introduction to Quantum Programming in Quipper. RC (2013)
Peter LeFanu Lumsdaine
Weak omega-categories from intensional type theory Log. Methods Comput. Sci. 6 (3) (2010)
Steven Awodey, Nicola Gambino, Peter LeFanu Lumsdaine, Michael A. Warren
Lawvere - Tierney sheaves in Algebraic Set Theory. J. Symb. Log. 74 (3) (2009)
Peter LeFanu Lumsdaine
Weak omega-Categories from Intensional Type Theory. TLCA (2009)