@unpublished(anel2017blakers,
 author       = {Mathieu Anel and Georg Biedermann and Eric Finster and Andr{\'e} Joyal},
 year         = {2017},
 title        = {A Generalized Blakers-Massey Theorem},
 url          = {https://arxiv.org/abs/1703.09050},
)
@unpublished(abcfhl17cart,
 author       = {Carlo Angiuli and Guillaume Brunerie and Thierry Coquand and {Hou (Favonia)}, Kuen-Bang and Robert Harper and Daniel R. Licata},
 year         = {2017},
 title        = {Cartesian Cubical Type Theory},
 url          = {https://github.com/dlicata335/cart-cube},
 note         = {Preprint},
)
@inproceedings(ahw2017cubical,
 author       = {Carlo Angiuli and Robert Harper and Todd Wilson},
 year         = {2017},
 title        = {Computational Higher-Dimensional Type Theory},
 booktitle    = {Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages},
 series       = {POPL 2017},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {680--693},
 doi          = {10.1145/3009837.3009861},
)
@unpublished(afh17uuee,
 author       = {Carlo Angiuli and {Hou (Favonia)}, Kuen-Bang and Robert Harper},
 year         = {2017},
 title        = {Computational Higher Type Theory {III}: Univalent Universes and Exact Equality},
 url          = {https://arxiv.org/abs/1712.01800},
)
@unpublished(ack17twolevel,
 author       = {Danil Annenkov and Paolo Capriotti and Nicolai Kraus},
 year         = {2017},
 title        = {Two-Level Type Theory and Applications},
 url          = {https://arxiv.org/abs/1705.03307},
)
@inproceedings(matita2011,
 author       = {Andrea Asperti and Wilmer Ricciotti and Claudio Sacerdoti Coen and Enrico Tassi},
 year         = {2011},
 title        = {The Matita Interactive Theorem Prover},
 booktitle    = {Automated Deduction - {CADE-23} - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings},
 pages        = {64--69},
 doi          = {10.1007/978-3-642-22438-6_7},
)
@techreport(bates:1981,
 author       = {Joseph L. Bates},
 year         = {1981},
 title        = {A Logic for Correct Program Development},
 type         = {Technical Report},
 number       = {TR81-455},
 institution  = {Cornell University},
 url          = {http://hdl.handle.net/1813/6295},
 note         = {Revision of Cornell University Ph.D. thesis submitted August 1979},
)
@inproceedings(coqhott,
 author       = {Andrej Bauer and Jason Gross and Peter LeFanu Lumsdaine and Michael Shulman and Matthieu Sozeau and Bas Spitters},
 year         = {2017},
 title        = {The {HoTT} Library: A Formalization of Homotopy Type Theory in Coq},
 booktitle    = {Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs},
 series       = {CPP 2017},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {164--172},
 doi          = {10.1145/3018610.3018615},
)
@inproceedings(bch,
 author       = {Marc Bezem and Thierry Coquand and Simon Huber},
 year         = {2014},
 title        = {A model of type theory in cubical sets},
 booktitle    = {19th International Conference on Types for Proofs and Programs (TYPES 2013)},
 volume       = {26},
 publisher    = {Dagstuhl Publishing},
 address      = {Toulouse, France},
 pages        = {107--128},
 doi          = {10.4230/LIPIcs.TYPES.2013.107},
)
@article(brady:2013,
 author       = {Edwin Brady},
 year         = {2013},
 title        = {{Idris}, a general-purpose dependently typed programming language: Design and implementation},
 journal      = {Journal of Functional Programming},
 volume       = {23},
 number       = {5},
 pages        = {552--593},
 doi          = {10.1017/S095679681300018X},
)
@phdthesis(brunerie2016homotopy,
 author       = {Guillaume Brunerie},
 year         = {2016},
 title        = {On the homotopy groups of spheres in homotopy type theory},
 school       = {Université Nice Sophia Antipolis},
 url          = {https://arxiv.org/abs/1606.05916},
)
@misc(agdahott,
 author       = {Guillaume Brunerie and {Hou (Favonia)}, Kuen-Bang and Evan Cavallo and Eric Finster and Jesper Cockx and Christian Sattler and Chris Jeris and Michael Shulman},
 year         = {2018},
 title        = {Homotopy Type Theory in {A}gda},
 url          = {https://github.com/HoTT/HoTT-Agda},
)
@unpublished(ch18inductive,
 author       = {Evan Cavallo and Robert Harper},
 year         = {2018},
 title        = {Computational Higher Type Theory {IV}: Inductive Types},
 url          = {https://arxiv.org/abs/1801.01568},
)
@inproceedings(cohen2018cubical,
 author       = {Cyril Cohen and Thierry Coquand and Simon Huber and Anders M{\"o}rtberg},
 year         = {2018},
 title        = {{Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom}},
 booktitle    = {21st International Conference on Types for Proofs and Programs (TYPES 2015)},
 volume       = {69},
 publisher    = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
 address      = {Dagstuhl, Germany},
 pages        = {5:1--5:34},
 doi          = {10.4230/LIPIcs.TYPES.2015.5},
)
@misc(cubicaltt,
 author       = {Cyril Cohen and Thierry Coquand and Simon Huber and Anders M{\"o}rtberg},
 year         = {2018},
 title        = {\texttt{cubicaltt}: Experimental implementation of {Cubical Type Theory}},
 howpublished = {\url{https://github.com/mortberg/cubicaltt}},
)
@book(constableetalnuprl,
 author       = {{Constable, et al.}, Robert L.},
 year         = {1985},
 title        = {Implementing Mathematics with the Nuprl Proof Development Environment},
 publisher    = {Prentice-Hall},
 address      = {Englewood Cliffs, NJ},
 url          = {http://www.nuprl.org/book/},
)
@inproceedings(leanhott,
 author       = {Floris van Doorn and Jakob von Raumer and Ulrik Buchholtz},
 year         = {2017},
 title        = {Homotopy Type Theory in Lean},
 booktitle    = {Interactive Theorem Proving},
 publisher    = {Springer},
 address      = {Cham},
 pages        = {479--495},
 doi          = {10.1007/978-3-319-66107-0_30},
)
@book(gordon-milner-wadsworth:1979,
 author       = {Michael Gordon and Robin Milner and Christopher Wadsworth},
 year         = {1979},
 title        = {Edinburgh {LCF}: A Mechanized Logic of Computation},
 series       = {Lecture Notes in Computer Science},
 volume       = {78},
 publisher    = {Springer-Verlag},
 address      = {Berlin, Heidelberg},
 doi          = {10.1007/3-540-09724-4},
)
@unpublished(kapulkinlumsdaine,
 author       = {Chris Kapulkin and Peter LeFanu Lumsdaine},
 year         = {2016},
 title        = {The Simplicial Model of Univalent Foundations (after {V}oevodsky)},
 url          = {https://arxiv.org/abs/1211.2851},
)
@misc(licata2014cubical,
 author       = {Daniel R. Licata and Guillaume Brunerie},
 year         = {2014},
 title        = {A cubical type theory},
 url          = {http://dlicata.web.wesleyan.edu/pubs/lb14cubical/lb14cubes-oxford.pdf},
 note         = {Talk at Oxford Homotopy Type Theory Workshop},
)
@unpublished(lumsdaineshulman,
 author       = {Peter LeFanu Lumsdaine and Mike Shulman},
 year         = {2017},
 title        = {Semantics of higher inductive types},
 url          = {https://arxiv.org/abs/1705.07088},
)
@article(cmcp,
 author       = {{Martin-L\"{o}f}, P.},
 year         = {1984},
 title        = {Constructive Mathematics and Computer Programming},
 journal      = {Philosophical Transactions of the Royal Society of London Series A},
 volume       = {312},
 pages        = {501--518},
 doi          = {10.1098/rsta.1984.0073},
)
@inproceedings(mcbride:2004,
 author       = {Conor McBride},
 year         = {2005},
 title        = {Epigram: Practical Programming with Dependent Types},
 booktitle    = {Proceedings of the 5th International Conference on Advanced Functional Programming},
 series       = {AFP'04},
 publisher    = {Springer-Verlag},
 address      = {Berlin, Heidelberg},
 pages        = {130--170},
 doi          = {10.1007/11546382_3},
)
@phdthesis(spiwack2011,
 author       = {Arnaud Spiwack},
 year         = {2011},
 title        = {Verified Computing in Homological Algebra, A Journey Exploring the Power and Limits of Dependent Type Theory},
 school       = {\'Ecole Polytechnique},
 url          = {https://pastel.archives-ouvertes.fr/pastel-00605836},
)
@unpublished(sterling2017,
 author       = {Jonathan Sterling and Robert Harper},
 year         = {2017},
 title        = {{Algebraic Foundations of Proof Refinement}},
 url          = {https://arxiv.org/abs/1703.05215},
)
@misc(redprl,
 author       = {{The RedPRL Development Team}},
 year         = {2018},
 title        = {{RedPRL} -- the {P}eople's {R}efinement {L}ogic},
 url          = {http://www.redprl.org/},
)
@book(hottbook,
 author       = {{Univalent Foundations Program}, The},
 year         = {2013},
 title        = {Homotopy Type Theory: Univalent Foundations of Mathematics},
 publisher    = {\url{http://homotopytypetheory.org/book}},
 address      = {Institute for Advanced Study},
)
@misc(voevodskycmu,
 author       = {Vladimir Voevodsky},
 year         = {2010},
 title        = {The equivalence axiom and univalent models of type theory},
 url          = {http://www.math.ias.edu/vladimir/files/CMU_talk.pdf},
 note         = {Notes from a talk at Carnegie Mellon University},
)
@unpublished(voevodsky10hcanon,
 author       = {Vladimir Voevodsky},
 year         = {2010},
 title        = {Univalent Foundations Project},
 url          = {http://www.math.ias.edu/vladimir/files/univalent_foundations_project.pdf},
 note         = {Modified version of an NSF grant application},
)
@unpublished(voevodsky13hts,
 author       = {Vladimir Voevodsky},
 year         = {2013},
 title        = {A type system with two kinds of identity types},
 url          = {https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/HTS.pdf},
 note         = {Slides available at \url{https://uf-ias-2012.wikispaces.com/file/view/HTS_slides.pdf/410105196/HTS_slides.pdf}},
)