References (Rev #4, changes)

Showing changes from revision #3 to #4:
Added | ~~Removed~~ | ~~Chan~~ged

A roughly taxonomised listing of some of the papers on Homotopy Type Theory. Titles link to more details, bibdata, etc. Currently very incomplete; please add!

*Type theory and homotopy.*Steve Awodey, 2010. (To appear.) PDF*Homotopy type theory and Voevodsky?s univalent foundations.*Álvaro Pelayo and Michael A. Warren, 2012. (Bulletin of the AMS, forthcoming) arXiv*Voevodsky?s Univalence Axiom in homotopy type theory.*Steve Awodey, Álvaro Pelayo, and Michael A. Warren, October 2013, Notices of the American Mathematical Society 60(08), pp.1164-1167. arXiv

*The groupoid interpretation of type theory.*Thomas Streicher and Martin Hofmann, in Sambin (ed.) et al., Twenty-five years of constructive type theory. Proceedings of a congress, Venice, Italy, October 19?21, 1995. Oxford: Clarendon Press. Oxf. Logic Guides. 36, 83-111 (1998). PostScript*Homotopy theoretic models of identity types.*Steve Awodey and Michael Warren, Mathematical Proceedings of the Cambridge Philosophical Society, 2009. PDF*Homotopy theoretic aspects of constructive type theory.*Michael A. Warren, Ph.D. thesis: Carnegie Mellon University, 2008. PDF*Two-dimensional models of type theory*, Richard Garner, Mathematical Structures in Computer Science 19 (2009), no. 4, pages 687?736. RG?s website*Topological and simplicial models of identity types.*Richard Garner and Benno van den Berg, to appear in ACM Transactions on Computational Logic (TOCL). PDF*The strict ∞-groupoid interpretation of type theory*Michael Warren, in Models, Logics and Higher-Dimensional Categories: A Tribute to the Work of Mihály Makkai, AMS/CRM, 2011. PDF*Homotopy-Theoretic Models of Type Theory.*Peter Arndt and Chris Kapulkin. In Typed Lambda Calculi and Applications, volume 6690 of Lecture Notes in Computer Science, pages 45?60.*Combinatorial realizability models of type theory*, Pieter Hofstra and Michael A. Warren, 2013, Annals of Pure and Applied Logic 164(10), pp. 957-988. arXiv

*Univalence in simplicial sets.*Chris Kapulkin, Peter LeFanu Lumsdaine, Vladimir Voevodsky. arXiv*Univalence for inverse diagrams and homotopy canonicity.*Michael Shulman. arXiv*Fiber bundles and univalence.*Lecture by Ieke Moerdijk at the Lorentz Center, Leiden, December 2011. Lecture notes by Chris Kapulkin*A model of type theory in simplicial sets: A brief introduction to Voevodsky?s homotopy type theory.*Thomas Streicher, 2011. PDF*Univalence and Function Extensionality.*Lecture by Nicola Gambino at Oberwohlfach, February 2011. Lecture notes by Chris Kapulkin and Peter Lumsdaine*The Simplicial Model of Univalent Foundations.*Chris Kapulkin and Peter LeFanu Lumsdaine and Vladimir Voevodsky, 2012. arXiv*The univalence axiom for elegant Reedy presheaves*. Michael Shulman, arXiv*A univalent universe in finite order arithmetic*. Colin McLarty, arXiv*Realizability of Univalence: Modest Kan complexes*. Wouter Pieter Stekelenburg, arXiv

*Inductive Types in Homotopy Type Theory.*S. Awodey, N. Gambino, K. Sojakova. To appear in LICS 2012. arXiv*W-types in homotopy type theory*. Benno van den Berg and Ieke Moerdijk, arXiv*Homotopy-initial algebras in type theory*Steve Awodey, Nicola Gambino, Kristina Sojakova. arXiv, Coq code

*A preliminary univalent formalization of the p-adic numbers.*Álvaro Pelayo, Vladimir Voevodsky, Michael A. Warren, 2012. arXiv

*Calculating the fundamental group of the circle in homotopy type theory*. Dan Licata and Michael Shulman, LICS 2013, available here and on arXiv*Eilenberg-MacLane Spaces in Homotopy Type Theory*. Dan Licata and Eric Finster, PDF and code

*Homotopical patch theory*. Carlo Angiuli, Ed Morehouse, Dan Licata, Robert Harper, PDF

*A Cubical Approach to Synthetic Homotopy Theory*. Dan Licata and Guillaume Brunerie, PDF*A syntax for cubical type theory*. Thorsten Altenkirch and Ambrus Kaposi, PDF*Implementation of Univalence in Cubical Sets*, github*A Note on the Uniform Kan Condition in Nominal Cubical Sets*, Robert Harper and Kuen-Bang Hou. arXiv

*The identity type weak factorisation system.*Nicola Gambino and Richard Garner, Theoretical Computer Science 409 (2008), no. 3, pages 94?109. RG?s website*Types are weak ∞-groupoids.*Richard Garner and Benno van den Berg, to appear. RG?s website*Weak ∞-Categories from Intensional Type Theory.*Peter LeFanu Lumsdaine, TLCA 2009, Brasília, Logical Methods in Computer Science, Vol. 6, issue 23, paper 24. PDF*Higher Categories from Type Theories.*Peter LeFanu Lumsdaine, PhD Thesis: Carnegie Mellon University, 2010. PDF*A coherence theorem for Martin-Löf?s type theory.*Michael Hedberg, Journal of Functional Programming 8 (4): 413?436, July 1998.*Model Structures from Higher Inductive Types.*P. LeFanu Lumsdaine. Unpublished note, Dec. 2011. PDF*A category-theoretic version of the identity type weak factorization system*. Jacopo Emmenegger, arXiv

*Canonicity for 2-Dimensional Type Theory.*Dan Licata and Robert Harper. POPL 2012. PDF

*Martin-Löf Complexes.*S. Awodey, P. Hofstra and M.A. Warren, 2013, Annals of Pure and Applied Logic, 164(10), pp. 928-956. PDF, arXiv*2-Dimensional Directed Dependent Type Theory.*Dan Licata and Robert Harper. MFPS 2011. See also Chapters 7 and 8 of Dan?s thesis. PDF

Revision on June 29, 2015 at 14:52:11 by Mike Shulman. See the history of this page for a list of all contributions to it.