@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}},
)