Peter LeFanu Lumsdaine

According to our database, Peter LeFanu Lumsdaine authored at least 18 papers between 2009 and 2023.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2023

Special issue on homotopy type theory 2019 vol. 2.

Dan Licata, Peter LeFanu Lumsdaine

Math. Struct. Comput. Sci., 2023

2021

Special issue on homotopy type theory 2019.

Dan Licata, Peter LeFanu Lumsdaine

Math. Struct. Comput. Sci., 2021

2020

A general definition of dependent type theories.

Andrej Bauer, Philipp G. Haselwarter, Peter LeFanu Lumsdaine

CoRR, 2020

2019

Displayed Categories.

Benedikt Ahrens, Peter LeFanu Lumsdaine

Log. Methods Comput. Sci., 2019

Constructive reflectivity Principles for Regular Theories.

Henrik Forssell, Peter LeFanu Lumsdaine

J. Symb. Log., 2019

Preface: Special Issue on Homotopy Type Theory and Univalent Foundations.

Peter LeFanu Lumsdaine, Nicolas Tabareau

J. Autom. Reason., 2019

2018

Categorical structures for type theory in univalent foundations.

Benedikt Ahrens, Peter LeFanu Lumsdaine, Vladimir Voevodsky

Log. Methods Comput. Sci., 2018

Formalization of Mathematics in Type Theory (Dagstuhl Seminar 18341).

Andrej Bauer, Martín Hötzel Escardó, Peter LeFanu Lumsdaine, Assia Mahboubi

Dagstuhl Reports, 2018

2017

The HoTT library: a formalization of homotopy type theory in Coq.

Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, Bas Spitters

Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017

2016

Parametricity, Automorphisms of the Universe, and Excluded Middle.

Auke Bart Booij, Martín Hötzel Escardó, Peter LeFanu Lumsdaine, Michael Shulman

Proceedings of the 22nd International Conference on Types for Proofs and Programs, 2016

A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory.

Kuen-Bang Hou (Favonia), Eric Finster, Daniel R. Licata, Peter LeFanu Lumsdaine

Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

2015

The Local Universes Model: An Overlooked Coherence Construction for Dependent Type Theories.

Peter LeFanu Lumsdaine, Michael A. Warren

ACM Trans. Comput. Log., 2015

Homotopy limits in type theory.

Jeremy Avigad, Krzysztof Kapulkin, Peter LeFanu Lumsdaine

Math. Struct. Comput. Sci., 2015

2013

Homotopy limits in Coq

Jeremy Avigad, Krzysztof Kapulkin, Peter LeFanu Lumsdaine

CoRR, 2013

An Introduction to Quantum Programming in Quipper.

Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, Benoît Valiron

Proceedings of the Reversible Computation - 5th International Conference, 2013

Quipper: a scalable quantum programming language.

Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, Benoît Valiron

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2013

2010

Weak omega-categories from intensional type theory

Peter LeFanu Lumsdaine

Log. Methods Comput. Sci., 2010

2009

Lawvere - Tierney sheaves in Algebraic Set Theory.

Steven Awodey, Nicola Gambino, Peter LeFanu Lumsdaine, Michael A. Warren

J. Symb. Log., 2009