1. Mathieu Anel, Georg Biedermann, Eric Finster & André Joyal (2017): A Generalized Blakers-Massey Theorem. Available at
  2. Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Kuen-Bang Hou (Favonia), Robert Harper & Daniel R. Licata (2017): Cartesian Cubical Type Theory. Available at Preprint.
  3. Carlo Angiuli, Robert Harper & Todd Wilson (2017): Computational Higher-Dimensional Type Theory. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017. ACM, New York, NY, USA, pp. 680–693, doi:10.1145/3009837.3009861.
  4. Carlo Angiuli, Kuen-Bang Hou (Favonia) & Robert Harper (2017): Computational Higher Type Theory III: Univalent Universes and Exact Equality. Available at
  5. Danil Annenkov, Paolo Capriotti & Nicolai Kraus (2017): Two-Level Type Theory and Applications. Available at
  6. Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen & Enrico Tassi (2011): The Matita Interactive Theorem Prover. In: Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings, pp. 64–69, doi:10.1007/978-3-642-22438-6_7.
  7. Joseph L. Bates (1981): A Logic for Correct Program Development. Technical Report TR81-455. Cornell University. Available at Revision of Cornell University Ph.D. thesis submitted August 1979.
  8. Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau & Bas Spitters (2017): The HoTT Library: A Formalization of Homotopy Type Theory in Coq. In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017. ACM, New York, NY, USA, pp. 164–172, doi:10.1145/3018610.3018615.
  9. Marc Bezem, Thierry Coquand & Simon Huber (2014): A model of type theory in cubical sets. In: 19th International Conference on Types for Proofs and Programs (TYPES 2013) 26. Dagstuhl Publishing, Toulouse, France, pp. 107–128, doi:10.4230/LIPIcs.TYPES.2013.107.
  10. Edwin Brady (2013): Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming 23(5), pp. 552–593, doi:10.1017/S095679681300018X.
  11. Guillaume Brunerie (2016): On the homotopy groups of spheres in homotopy type theory. Université Nice Sophia Antipolis. Available at
  12. Guillaume Brunerie, Kuen-Bang Hou (Favonia), Evan Cavallo, Eric Finster, Jesper Cockx, Christian Sattler, Chris Jeris & Michael Shulman (2018): Homotopy Type Theory in Agda. Available at
  13. Evan Cavallo & Robert Harper (2018): Computational Higher Type Theory IV: Inductive Types. Available at
  14. Cyril Cohen, Thierry Coquand, Simon Huber & Anders Mörtberg (2018): Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In: 21st International Conference on Types for Proofs and Programs (TYPES 2015) 69. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, pp. 5:1–5:34, doi:10.4230/LIPIcs.TYPES.2015.5.
  15. Cyril Cohen, Thierry Coquand, Simon Huber & Anders Mörtberg (2018): cubicaltt: Experimental implementation of Cubical Type Theory.
  16. Robert L. Constable, et al. (1985): Implementing Mathematics with the Nuprl Proof Development Environment. Prentice-Hall, Englewood Cliffs, NJ. Available at
  17. Floris van Doorn, Jakob von Raumer & Ulrik Buchholtz (2017): Homotopy Type Theory in Lean. In: Interactive Theorem Proving. Springer, Cham, pp. 479–495, doi:10.1007/978-3-319-66107-0_30.
  18. Michael Gordon, Robin Milner & Christopher Wadsworth (1979): Edinburgh LCF: A Mechanized Logic of Computation. Lecture Notes in Computer Science 78. Springer-Verlag, Berlin, Heidelberg, doi:10.1007/3-540-09724-4.
  19. Chris Kapulkin & Peter LeFanu Lumsdaine (2016): The Simplicial Model of Univalent Foundations (after Voevodsky). Available at
  20. Daniel R. Licata & Guillaume Brunerie (2014): A cubical type theory. Available at Talk at Oxford Homotopy Type Theory Workshop.
  21. Peter LeFanu Lumsdaine & Mike Shulman (2017): Semantics of higher inductive types. Available at
  22. P. Martin-Löf (1984): Constructive Mathematics and Computer Programming. Philosophical Transactions of the Royal Society of London Series A 312, pp. 501–518, doi:10.1098/rsta.1984.0073.
  23. Conor McBride (2005): Epigram: Practical Programming with Dependent Types. In: Proceedings of the 5th International Conference on Advanced Functional Programming, AFP'04. Springer-Verlag, Berlin, Heidelberg, pp. 130–170, doi:10.1007/11546382_3.
  24. Arnaud Spiwack (2011): Verified Computing in Homological Algebra, A Journey Exploring the Power and Limits of Dependent Type Theory. École Polytechnique. Available at
  25. Jonathan Sterling & Robert Harper (2017): Algebraic Foundations of Proof Refinement. Available at
  26. The RedPRL Development Team (2018): RedPRL – the People's Refinement Logic. Available at
  27. The Univalent Foundations Program (2013): Homotopy Type Theory: Univalent Foundations of Mathematics., Institute for Advanced Study.
  28. Vladimir Voevodsky (2010): The equivalence axiom and univalent models of type theory. Available at Notes from a talk at Carnegie Mellon University.
  29. Vladimir Voevodsky (2010): Univalent Foundations Project. Available at Modified version of an NSF grant application.
  30. Vladimir Voevodsky (2013): A type system with two kinds of identity types. Available at Slides available at

Comments and questions to:
For website issues: