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!
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. (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
General models:
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 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:
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
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
Univalence for inverse EI diagrams. Michael shulman, arXiv
Inductive and higher-inductive types
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
The General Universal Property of the Propositional Truncation. Nicolai Kraus, arXiv
Formalizations of set-level mathematics
A preliminary univalent formalization of the p-adic numbers. Álvaro Pelayo, Vladimir Voevodsky, Michael A. Warren, 2012. arXiv
Univalent categories and the Rezk completion. Benedikt Ahrens, Chris Kapulkin, Michael Shulman, Math. Structures Comput. Sci. 25 (2015), no. 5, 1010?1039. arXiv
Synthetic homotopy theory
Calculating the fundamental group of the circle in homotopy type theory. Dan Licata and Michael Shulman, LICS 2013, available here and on arXiv
Homotopy limits in type theory. Jeremy Avigad, Chris Kapulkin, Peter LeFanu Lumsdaine, Math. Structures Comput. Sci. 25 (2015), no. 5, 1040?1070. arXiv
Eilenberg-MacLane Spaces in Homotopy Type Theory. Dan Licata and Eric Finster, PDF and code
Homotopical ideas and truncations in type theory
Notions of anonymous existence in Martin-Lof type theory. Nicolai Kraus, Martín Escardó, Thierry Coquand, and Thorsten Altenkirch. pdf
Idempotents in intensional type theory. Michael Shulman, arXiv
Applications to computing
Homotopical patch theory. Carlo Angiuli, Ed Morehouse, Dan Licata, Robert Harper, PDF
Cubical models and cubical type theory
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
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