ref.bib

@book{MLTT,
  title = {Intuitionistic type theory},
  author = {Martin-L\"of, P. and Sambin, G.},
  series = {Studies in proof theory},
  url = {https://books.google.com/books?id=\_D0ZAQAAIAAJ},
  year = {1984},
  publisher = {Bibliopolis},
  address = {Napoli, Italy},
}

@Book{hottbook,
  author = {The {Univalent Foundations Program}},
  title = {Homotopy Type Theory: Univalent Foundations of Mathematics},
  publisher = {\url { https://homotopytypetheory.org/book }},
  address = {Institute for Advanced Study},
  year = 2013,
}

@phdthesis{Agda,
  author = {Norell, Ulf},
  school = {{ Chalmers, G\"oteborg University }},
  title = {Towards a practical programming language based on dependent type theory},
  year = {2007},
}

@online{AgdaHoTT,
  author={Guillaume Brunerie
    and Kuen-Bang {Hou (Favonia)}
    and Evan Cavallo
    and Tim Baumann
    and Eric Finster
    and Jesper Cockx
    and Christian Sattler
    and Chris Jeris
    and Michael Shulman
    and others},
  title={Homotopy Type Theory in {A}gda},
  howpublished={\url{https://github.com/HoTT/HoTT-Agda}},
  url={https://github.com/HoTT/HoTT-Agda},
}

@article{PropWithoutK,
  author = {Gilbert, Ga\"etan and Cockx, Jesper and Sozeau, Matthieu and Tabareau, Nicolas},
  title = {Definitional Proof-irrelevance Without K},
  journal = {Proc. ACM Program. Lang.},
  issue_date = {January 2019},
  volume = {3},
  number = {POPL},
  month = jan,
  year = {2019},
  issn = {2475-1421},
  pages = {3:1--3:28},
  articleno = {3},
  numpages = {28},
  url = {http://doi.acm.org/10.1145/3290316},
  doi = {10.1145/3290316},
  acmid = {3290316},
  publisher = {ACM},
  address = {New York, NY, USA},
  keywords = {proof assistants, proof irrelevance, type theory},
}

@article{RewriteWithoutK,
  title = {Sprinkles of extensionality for your vanilla type theory},
  author = {Cockx, Jesper and Abel, Andreas},
  journal = {Abstract of a talk at TYPES},
  year = {2016}
}

@article{Idris,
  author = {BRADY,EDWIN},
  title = {Idris, a general-purpose dependently typed programming language: Design and implementation},
  journal = {Journal of Functional Programming},
  volume = {23},
  issue = {05},
  month = {9},
  year = {2013},
  issn = {1469-7653},
  pages = {552--593},
  numpages = {42},
  doi = {10.1017/S095679681300018X},
  URL = {http://journals.cambridge.org/article_S095679681300018X},
}

@misc{IdrisHoTT,
  author = {Francisco Mota and Philip Dorrell},
  title = {A small, incomplete, and inconsistent formalization of homotopy type theory in Idris},
  year = {2017},
  publisher = {GitHub},
  journal = {GitHub repository},
  howpublished = {\url{https://github.com/associahedron/HoTT-Idris}},
  commit = {59feb06fc311d94278b8e22bd521dbea5c3312d7}
}

@article{HottCoq,
  author    = {Andrej Bauer and
               Jason Gross and
               Peter LeFanu Lumsdaine and
               Michael Shulman and
               Matthieu Sozeau and
               Bas Spitters},
  title     = {The HoTT Library: {A} formalization of homotopy type theory in Coq},
  journal   = {CoRR},
  volume    = {abs/1610.04591},
  year      = {2016},
  url       = {http://arxiv.org/abs/1610.04591},
  archivePrefix = {arXiv},
  eprint    = {1610.04591},
  timestamp = {Mon, 13 Aug 2018 16:48:11 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/BauerGLSSS16},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@misc{Mlang,
  author = {Minghao Liu},
  title = {A cubical type theory implementation with implicit arguments, structural record and sum types and more},
  year = {2019},
  publisher = {GitHub},
  journal = {GitHub repository},
  howpublished = {\url{https://github.com/molikto/mlang}},
  commit = {5718d9a4ad59f7881c1b1ff7f441a0d114116aeb}
}

@misc{CubicalTT,
  author = {Anders M\"ortberg},
  title = {Experimental implementation of Cubical Type Theory in which the user can directly manipulate n-dimensional cubes},
  year = {2018},
  publisher = {GitHub},
  journal = {GitHub repository},
  howpublished = {\url{https://github.com/mortberg/cubicaltt}},
  commit = {a5c6f94bfc0da84e214641e0b87aa9649ea114ea}
}

@misc{YaccTT,
  author = {Anders M\"ortberg and Carlo Angiuli},
  title = {Yet Another Cartesian Cubical Type Theory},
  year = {2018},
  publisher = {GitHub},
  journal = {GitHub repository},
  howpublished = {\url{https://github.com/mortberg/yacctt}},
  commit = {72cf5472764f89c1c978c72fb75f9b938dc17465}
}

@online{RedPRL,
  author = {Jon Sterling
            and Daniel Gratzer
            and Eugene Akentyev
            and James Wilcox
            and David Christiansen
            and Darin Morrison
            and Favonia
            and Evan Cavallo
            and Carlo Angiuli
            and Tim Baumann
            and Anders M\"ortberg},
  title = {The RedPRL Proof Assistant},
  year = {2019},
  howpublished = {\url{http://www.redprl.org}},
  url = {http://www.redprl.org},
}

@misc{RedTT,
  author = {Jonathan Sterling and Kuen-Bang {Hou (Favonia)} and Evan Cavallo and Carlo Angiuli},
  title = {``Between the darkness and the dawn, a red cube rises!'': a proof assistant for cartesian cubical type theory},
  year = {2019},
  publisher = {GitHub},
  journal = {GitHub repository},
  howpublished = {\url{https://github.com/RedPRL/redtt}},
  commit = {5069c89fb0cd8fc1936ac8aa1e5dd6f4c1691db4}
}

@article{OPModel,
  author    = {Ian Orton and Andrew M. Pitts},
  title     = {Axioms for Modelling Cubical Type Theory in a Topos},
  journal   = {CoRR},
  volume    = {abs/1712.04864},
  year      = {2017},
  url       = {http://arxiv.org/abs/1712.04864},
  archivePrefix = {arXiv},
  eprint    = {1712.04864},
  timestamp = {Mon, 13 Aug 2018 16:46:38 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1712-04864},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{CubicalAgda,
  author = {Vezzosi, Andrea and M\"ortberg, Anders and Abel, Andreas},
  title = {Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types},
  journal = {Proc. ACM Program. Lang.},
  issue_date = {August 2019},
  volume = {3},
  number = {ICFP},
  month = jul,
  year = {2019},
  issn = {2475-1421},
  pages = {87:1--87:29},
  articleno = {87},
  numpages = {29},
  url = {http://doi.acm.org/10.1145/3341691},
  doi = {10.1145/3341691},
  acmid = {3341691},
  publisher = {ACM},
  address = {New York, NY, USA},
  keywords = {Cubical Type Theory, Dependent Pattern Matching, Higher Inductive Types, Univalence},
}

@misc{CHTT,
  title = {Computational Higher Type Theory III: Univalent Universes and Exact Equality},
  author = {Carlo Angiuli and Kuen-Bang Hou and Robert Harper},
  year = {2017},
  eprint = {1712.01800},
  archivePrefix = {arXiv},
  primaryClass = {cs.LO}
}

@book{Coq,
  author = {{ Coq Development Team }},
  publisher = {INRIA-Rocquencourt},
  title = {The {C}oq Proof Assistant Reference Manual},
  year = {2012}
}

@misc{Arend,
  author = {Valery Isaev and Sergey Sinchuk and Fedor Part and Tesla Ice Zhang},
  note = {Documentation available at \url { https://arend-lang.github.io }},
  title = {Arend Theorem Prover},
  year = {2020}
}

@misc{HoTT-I,
  title={Models of Homotopy Type Theory with an Interval Type},
  author={Valery Isaev},
  year={2020},
  eprint={2004.14195},
  archivePrefix={arXiv},
  primaryClass={cs.LO}
}

@incollection{Inductive,
  author = {Thierry Coquand and Christine Paulin},
  booktitle = {COLOG-88 (Tallinn, 1988)},
  pages = {50--66},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Inductively defined types},
  volume = {416},
  year = {1990}
}

@article{CCHM,
  title = {Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom},
  author = {Cyril Cohen and Thierry Coquand and Simon Huber and Anders M\"ortberg},
  journal = {FLAP},
  year = {2015},
  volume = {4},
  pages = {3127-3170}
}

@article{CHM,
  title = {On Higher Inductive Types in Cubical Type Theory},
  ISBN = {9781450355834},
  url = {http://dx.doi.org/10.1145/3209108.3209197},
  DOI = {10.1145/3209108.3209197},
  journal = {Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science - LICS ’18},
  publisher = {ACM Press},
  author = {Coquand, Thierry and Huber, Simon and Mörtberg, Anders},
  year = {2018}
}

@article{CCTT,
  title = {Cartesian Cubical Type Theory},
  author = {Angiuli, Carlo and Brunerie, Guillaume and Coquand, Thierry and Kuen-Bang {Hou (Favonia)} and Harper, Robert and Licata, Daniel R},
  note = {Draft available at \url { https://www.cs.cmu.edu/~rwh/papers/uniform/uniform.pdf }},
  year = 2017
}

@article{CCTT2,
  title = {Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities},
  author = {Angiuli, Carlo and Kuen-Bang {Hou (Favonia)} and Harper, Robert},
  journal = {Computer Science Logic 2018},
  year = {2018}
}

@misc{AxiomK,
  author = {Thomas Streicher},
  note = {Habilitationsschrift, Ludwig-Maximilians-Universit\"at M\"unchen},
  title = {Investigations into intensional type theory},
  year = 1993
}

@inproceedings{WithoutK,
  author = {Cockx, Jesper and Devriese, Dominique and Piessens, Frank},
  title = {Pattern Matching Without K},
  booktitle = {Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming},
  series = {ICFP '14},
  year = {2014},
  isbn = {978-1-4503-2873-9},
  location = {Gothenburg, Sweden},
  pages = {257--268},
  numpages = {12},
  url = {http://doi.acm.org/10.1145/2628136.2628139},
  doi = {10.1145/2628136.2628139},
  acmid = {2628139},
  publisher = {ACM},
  address = {New York, NY, USA},
}