Peter LeFanu Lumsdaine

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