References

  1. Mathieu Anel, Georg Biedermann, Eric Finster & André Joyal (2017): A Generalized Blakers-Massey Theorem. Available at https://arxiv.org/abs/1703.09050.
  2. Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Kuen-Bang Hou (Favonia), Robert Harper & Daniel R. Licata (2017): Cartesian Cubical Type Theory. Available at https://github.com/dlicata335/cart-cube. 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 https://arxiv.org/abs/1712.01800.
  5. Danil Annenkov, Paolo Capriotti & Nicolai Kraus (2017): Two-Level Type Theory and Applications. Available at https://arxiv.org/abs/1705.03307.
  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 http://hdl.handle.net/1813/6295. 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 https://arxiv.org/abs/1606.05916.
  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 https://github.com/HoTT/HoTT-Agda.
  13. Evan Cavallo & Robert Harper (2018): Computational Higher Type Theory IV: Inductive Types. Available at https://arxiv.org/abs/1801.01568.
  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. https://github.com/mortberg/cubicaltt.
  16. Robert L. Constable, et al. (1985): Implementing Mathematics with the Nuprl Proof Development Environment. Prentice-Hall, Englewood Cliffs, NJ. Available at http://www.nuprl.org/book/.
  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 https://arxiv.org/abs/1211.2851.
  20. Daniel R. Licata & Guillaume Brunerie (2014): A cubical type theory. Available at http://dlicata.web.wesleyan.edu/pubs/lb14cubical/lb14cubes-oxford.pdf. Talk at Oxford Homotopy Type Theory Workshop.
  21. Peter LeFanu Lumsdaine & Mike Shulman (2017): Semantics of higher inductive types. Available at https://arxiv.org/abs/1705.07088.
  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 https://pastel.archives-ouvertes.fr/pastel-00605836.
  25. Jonathan Sterling & Robert Harper (2017): Algebraic Foundations of Proof Refinement. Available at https://arxiv.org/abs/1703.05215.
  26. The RedPRL Development Team (2018): RedPRL – the People's Refinement Logic. Available at http://www.redprl.org/.
  27. The Univalent Foundations Program (2013): Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book, Institute for Advanced Study.
  28. Vladimir Voevodsky (2010): The equivalence axiom and univalent models of type theory. Available at http://www.math.ias.edu/vladimir/files/CMU_talk.pdf. Notes from a talk at Carnegie Mellon University.
  29. Vladimir Voevodsky (2010): Univalent Foundations Project. Available at http://www.math.ias.edu/vladimir/files/univalent_foundations_project.pdf. Modified version of an NSF grant application.
  30. Vladimir Voevodsky (2013): A type system with two kinds of identity types. Available at https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/HTS.pdf. Slides available at https://uf-ias-2012.wikispaces.com/file/view/HTS_slides.pdf/410105196/HTS_slides.pdf.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org