A roughly taxonomised listing of some of the papers on Homotopy Type Theory. Titles link to more details, bibdata, etc.
Surveys:
- 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. (To appear.) [arXiv]
General models:
- The groupoid interpretation of type theory. T. Streicher and M. Hofmann, in Sambin, Giovanni (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. [arXiv]
Univalence:
- Univalence in simplicial sets. Chris Kapulkin, Peter LeFanu Lumsdaine, Vladimir Voevodsky. [arXiv]
- The univalence axiom for inverse diagrams. 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]
Syntax of type theory:
- 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.
Computational interpretation:
- Canonicity for 2-Dimensional Type Theory. Dan Licata and Robert Harper. POPL 2012. [PDF]
Other:
- Martin-Löf Complexes. S. Awodey, P. Hofstra and M.A. Warren, submitted, 2009. Preprint on the arXiv as arXiv:0906.4521 (math.LO). [PDF], [arXiv]
- Inductive Types in Homotopy Type Theory. S. Awodey, N. Gambino, K. Sojakova. To appear in LICS 2012. [arXiv]
- Model Structures from Higher Inductive Types. P. LeFanu Lumsdaine. Unpublished note, Dec. 2011. [PDF]
- 2-Dimensional Directed Dependent Type Theory. Dan Licata and Robert Harper. MFPS 2011. See also Chapters 7 and 8 of Dan’s thesis. [PDF]
To have a listing added, just leave a reply below.
