history.bib

@incollection{abramsky:1995:domain,
  title     = {Domain theory},
  author    = {Abramsky, Samson and Jung, Achim},
  booktitle = {Handbook of logic in computer science (vol. 3) semantic structures},
  year      = {1995}
}
@article{automath:1994:automath,
  title   = {Selected papers on Automath},
  author  = {R.P. Nederpelt and J.H. Herman Geuvers and R.C. de Vrijer and L.S. van Benthem Jutting and David Van Daalen},
  journal = {Studies in logic and the foundations of mathematics},
  year    = {1994},
  volume  = {133},
  pages   = {299--301}
}
@misc{cartwright:2016:domain,
  url       = {https://arxiv.org/abs/1605.05858},
  author    = {Cartwright, Robert and Parsons, Rebecca and AbdelGawad, Moez},
  title     = {Domain Theory: An Introduction},
  publisher = {arXiv},
  year      = {2016}
}
@article{church:1932:untyped,
  title   = {A Set of Postulates for the Foundation of Logic},
  author  = {Alonzo Church},
  journal = {Annals of Mathematics},
  year    = {1932},
  volume  = {33},
  pages   = {346}
}
@article{church:1936:lambda,
  title   = {An Unsolvable Problem of Elementary Number Theory},
  author  = {Alonzo Church},
  journal = {American Journal of Mathematics},
  year    = {1936},
  volume  = {58},
  pages   = {345}
}
@article{curry:1934:combinatorCH,
  author  = {H. B. Curry},
  title   = {Functionality in Combinatory Logic},
  journal = {Proceedings of the National Academy of Sciences},
  volume  = {20},
  number  = {11},
  pages   = {584-590},
  year    = {1934},
  url     = {https://www.pnas.org/doi/abs/10.1073/pnas.20.11.584}
}
@article{eberl:2018:pnt,
  author  = {Manuel Eberl and Lawrence C. Paulson},
  title   = {The Prime Number Theorem},
  journal = {Archive of Formal Proofs},
  month   = {9},
  year    = {2018},
  note    = {\url{https://isa-afp.org/entries/Prime_Number_Theorem.html},
             Formal proof development}
}
@article{farmer:2008:virtues,
  title   = {The seven virtues of simple type theory},
  journal = {Journal of Applied Logic},
  volume  = {6},
  number  = {3},
  pages   = {267-286},
  year    = {2008},
  url     = {https://www.sciencedirect.com/science/article/pii/S157086830700081X},
  author  = {William M. Farmer}
}
@book{friedman:2018:typer,
  title     = {The Little Typer},
  author    = {Friedman, Daniel P and Christiansen, David Thrane},
  publisher = {MIT Press},
  series    = {The MIT Press},
  month     = {9},
  year      = {2018},
  address   = {London, England}
}
@phdthesis{girard:1972:systemf,
  author = {Jean-Yves Girard},
  school = {Universit\'e Paris VII},
  title  = {Interpr\'etation fonctionnelle et \'elimination des cou\-pures dans l'arith\-m\'e\-tique d'ordre sup\'erieure},
  url    = {http://prl.ccs.neu.edu/img/g-thesis-1972.pdf},
  year   = {1972}
}
@book{hartshorne:1977:ag,
  author    = {Robin Hartshorne},
  editor    = {S. Axler and F. W. Gehring and K. A. Ribet},
  publisher = {Springer},
  title     = {Algebraic Geometry},
  year      = {1977}
}
@incollection{hofmann:1998:groupoid,
  author    = {Hofmann, Martin and Streicher, Thomas},
  title     = {{The groupoid interpretation of type theory}},
  booktitle = {{Twenty Five Years of Constructive Type Theory}},
  publisher = {Oxford University Press},
  year      = {1998},
  month     = {10},
  url       = {https://doi.org/10.1093/oso/9780198501275.003.0008}
}
@book{johnstone:2008:elephant,
  place     = {Oxford},
  title     = {Sketches of an Elephant: A topos theory compendium},
  publisher = {Oxford University Press},
  author    = {Johnstone, Peter T.},
  year      = {2003},
  volume    = {1}
}
@article{joyal:2019：topologie,
  title   = {Topo-logie},
  author  = {Mathieu Anel and Andr{\'e} Joyal},
  year    = {2019},
  journal = {New Spaces in Mathematics},
  url     = {http://mathieu.anel.free.fr/mat/doc/Anel-Joyal-Topo-logie.pdf}
}
@incollection{lawvere:1994:objective,
  editor    = {John Macnamara and Gonzalo E. Reyes},
  author    = {F. William Lawvere},
  publisher = {Oxford University Press USA},
  pages     = {43--56},
  booktitle = {The Logical Foundations of Cognition},
  title     = {Tools for the Advancement of Objective Logic: Closed Categories and Toposes},
  year      = {1994}
}
@article{lean:2020:mathlib,
  title   = {The lean mathematical library},
  author  = {The mathlib Community},
  journal = {Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs},
  year    = {2020}
}
@article{loader:1998:stlc,
  title  = {Notes on Simply Typed Lambda Calculus},
  author = {Ralph Loader},
  year   = {1998},
  url    = {http://www.lfcs.inf.ed.ac.uk/reports/98/ECS-LFCS-98-381/ECS-LFCS-98-381.pdf}
}
@inproceedings{maclane:1971:category,
  title  = {Categories for the working mathematician},
  author = {Saunders Maclane},
  year   = {1971}
}
@book{maclane:2012:sheaves,
  title     = {Sheaves in Geometry and Logic: A First Introduction to Topos Theory},
  author    = {MacLane, S. and Moerdijk, I.},
  series    = {Universitext},
  year      = {2012},
  publisher = {Springer New York}
}
@article{mclarty:1990:toposhistory,
  title   = {The Uses and Abuses of the History of Topos Theory},
  author  = {Colin McLarty},
  journal = {The British Journal for the Philosophy of Science},
  year    = {1990},
  volume  = {41},
  pages   = {351 - 375}
}
@misc{me:2022:lccc,
  url       = {https://arxiv.org/abs/2202.04543},
  author    = {Huang, Xu},
  title     = {Locally Cartesian Closed Categories},
  publisher = {arXiv},
  year      = {2022}
}
@inproceedings{reynolds:1974:systemf,
  title     = {Towards a theory of type structure},
  author    = {John C. Reynolds},
  booktitle = {Symposium on Programming},
  year      = {1974}
}
@inproceedings{reynolds:1984:polymorphism,
  title     = {Polymorphism is not Set-Theoretic},
  author    = {John C. Reynolds},
  booktitle = {Semantics of Data Types},
  year      = {1984}
}
@misc{scholze:2020:liquid,
  author       = {Peter Scholze},
  howpublished = {\url{https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-experiment/}},
  title        = {Liquid tensor experiment},
  year         = {2020}
}
@article{schonfinkel:1924:combinator,
  title   = {{\"U}ber die Bausteine der mathematischen Logik},
  author  = {Moses Sch{\"o}nfinkel},
  journal = {Mathematische Annalen},
  volume  = {92},
  pages   = {305-316},
  year    = {1924}
}
@article{seely:1984:lccc,
  title   = {Locally cartesian closed categories and type theory},
  author  = {Robert A. G. Seely},
  journal = {Mathematical Proceedings of the Cambridge Philosophical Society},
  year    = {1984},
  volume  = {95},
  pages   = {33 - 48}
}
@incollection{sep:2022:typetheory,
  author       = {Coquand, Thierry},
  title        = {{Type Theory}},
  booktitle    = {The {Stanford} Encyclopedia of Philosophy},
  editor       = {Edward N. Zalta and Uri Nodelman},
  howpublished = {\url{https://plato.stanford.edu/archives/fall2022/entries/type-theory/}},
  year         = {2022},
  edition      = {{F}all 2022},
  publisher    = {Metaphysics Research Lab, Stanford University}
}
@book{smullyan:1985:mockingbird,
  author    = {Raymond Smullyan},
  publisher = {Knopf},
  title     = {To Mock a Mockingbird and Other Logic Puzzles: Including an Amazing Adventure in Combinatory Logic},
  year      = {1985}
}
@phdthesis{sterling:2021:thesis,
  author = {Sterling, Jonathan},
  school = {Carnegie Mellon University},
  year   = {2021},
  doi    = {10.5281/zenodo.6990769},
  note   = {Version 1.1, revised May 2022},
  number = {CMU-CS-21-142},
  title  = {First Steps in Synthetic {Tait} Computability: The Objective Metatheory of Cubical Type Theory}
}
@book{tobias:2002:isabelle,
  author    = {Nipkow, Tobias and Paulson, Lawrence and Wenzel, Markus},
  year      = {2002},
  month     = {01},
  title     = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
  journal   = {Lecture Notes in Computer Science - LNCS},
  doi       = {10.1007/3-540-45949-9},
  publisher = {Springer}
}
@book{ufp:2013: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}
}
@unpublished{wadler:1990:free,
  author = {Philip Wadler},
  note   = {Unpublished manuscript},
  title  = {Recursive Types for Free!},
  year   = {1990},
  url    = {https://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt}
}
@misc{escardo:2018:univalence,
  url       = {https://arxiv.org/abs/1803.02294},
  author    = {Escardó, Martín Hötzel},
  title     = {A self-contained, brief and complete formulation of Voevodsky's Univalence Axiom},
  publisher = {arXiv},
  year      = {2018}
}
@article{awodey:2013:structuralism,
  author  = {Awodey, Steve},
  title   = {Structuralism, Invariance, and Univalence},
  journal = {Philosophia Mathematica},
  volume  = {22},
  number  = {1},
  pages   = {1-11},
  year    = {2013},
  month   = {10},
  url     = {https://doi.org/10.1093/philmat/nkt030}
}
@misc{brunerie:2016:number,
  url       = {https://arxiv.org/abs/1606.05916},
  author    = {Brunerie, Guillaume},
  title     = {On the homotopy groups of spheres in homotopy type theory},
  publisher = {arXiv},
  year      = {2016}
}
@inproceedings{barendregt:1992:lambda,
  title     = {Lambda calculi with types},
  author    = {Barendregt, Henk P},
  year      = {1992},
  publisher = {Oxford: Clarendon Press},
  url       = {http://www.cosc.brocku.ca/~mwinter/Courses/5P05/HBKJ.pdf}
}
@misc{winterhalter:2018:ettwtt,
  author       = {Théo Winterhalter and Matthieu Sozeau and Nicolas Tabareau},
  howpublished = {\url{https://github.com/TheoWinterhalter/ett-to-itt}},
  title        = {Eliminating Reflection from Type Theory},
  year         = {2018}
}
@thesis{streicher:1993:K,
  author      = {Thomas Streicher},
  title       = {Investigations into Intensional Type Theory},
  type        = {Habilitation thesis},
  institution = {Ludwig Maximilian University of Munich},
  year        = {2019},
  url         = {https://www2.mathematik.tu-darmstadt.de/~streicher/HabilStreicher.pdf}
}
@article{martinlof:1984:J,
  title   = {Constructive mathematics and computer programming},
  author  = {Per Martin-L{\"o}f},
  journal = {Studies in logic and the foundations of mathematics},
  year    = {1984},
  volume  = {104},
  pages   = {167-184},
  url     = {https://www.cs.tufts.edu/~nr/cs257/archive/per-martin-lof/constructive-math.pdf}
}
@article{boulier:2017:syntacticmodel,
  title   = {The next 700 syntactical models of type theory},
  author  = {Simon Pierre Boulier and Pierre-Marie P{\'e}drot and Nicolas Tabareau},
  journal = {Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs},
  year    = {2017}
}
@book{smith:2018:category,
  author    = {Peter Smith},
  publisher = {Logic Matters, Cambridge},
  title     = {Category Theory I: Notes towards a gentle introduction},
  year      = {2023},
  url       = {https://www.logicmatters.net/resources/pdfs/SmithCat-I.pdf}
}

@article{Lawvere:1963:functorial,
  title   = {Functorial Semantics of Algebraic Theories},
  author  = {F. William Lawvere},
  journal = {Proceedings of the National Academy of Sciences of the United States of America},
  year    = {1963},
  volume  = {50},
  pages   = {869-872}
}
@article{carl:1998:brouwer,
  title   = {Brouwer versus Hilbert: 1907–1928},
  author  = {J. Posy Carl},
  journal = {Science in Context},
  year    = {1998},
  volume  = {11},
  pages   = {291 - 325}
}
@incollection{sep:2022:constructive,
  author       = {Bridges, Douglas and Palmgren, Erik and Ishihara, Hajime},
  title        = {{Constructive Mathematics}},
  booktitle    = {The {Stanford} Encyclopedia of Philosophy},
  editor       = {Edward N. Zalta and Uri Nodelman},
  howpublished = {\url{https://plato.stanford.edu/archives/fall2022/entries/mathematics-constructive/}},
  year         = {2022},
  edition      = {{F}all 2022},
  publisher    = {Metaphysics Research Lab, Stanford University}
}
@book{brouwer:1981:intuitionism,
  title     = {Brouwer's Cambridge lectures on intuitionism},
  author    = {Luitzen Egbertus Jan Brouwer},
  editor    = {Dirk van Dalen},
  year      = {1981},
  publisher = {Cambridge University Press}
}
@article{bauer:2016:fivestage,
  title   = {Five stages of accepting constructive mathematics},
  author  = {Andrej Bauer},
  journal = {Bulletin of the American Mathematical Society},
  year    = {2016},
  volume  = {54},
  pages   = {481-498}
}
@book{beeson:1985:constructive,
  author    = {Michael J. Beeson},
  publisher = {Springer Berlin, Heidelberg},
  title     = {Foundations of Constructive Mathematics},
  year      = {1985}
}
@misc{blechschmidt:2021:internal,
  url       = {https://arxiv.org/abs/2111.03685},
  author    = {Ingo Blechschmidt},
  title     = {Using the internal language of toposes in algebraic geometry},
  publisher = {arXiv},
  year      = {2021}
}
@misc{bch:2017:cubical,
  url       = {https://arxiv.org/abs/1710.10941},
  author    = {Bezem, Marc and Coquand, Thierry and Huber, Simon},
  title     = {The univalence axiom in cubical sets},
  publisher = {arXiv},
  year      = {2017}
}
@article{cchm:2015:cubical,
  title   = {Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom},
  author  = {Cyril Cohen and Thierry Coquand and Simon Huber and Anders M{\"o}rtberg},
  journal = {FLAP},
  year    = {2015},
  volume  = {4},
  pages   = {3127-3170}
}
@article{abcfhl:2021:cubical,
  title   = {Syntax and models of Cartesian cubical type theory},
  author  = {Carlo Angiuli and Guillaume Brunerie and Thierry Coquand and Robert Harper and Kuen-Bang Hou (Favonia) and Daniel R. Licata},
  journal = {Mathematical Structures in Computer Science},
  year    = {2021},
  volume  = {31},
  pages   = {424 - 468}
}
@article{bezem:2015:simplicial,
  title   = {A Kripke model for simplicial sets},
  author  = {Marc Bezem and Thierry Coquand},
  journal = {Theor. Comput. Sci.},
  year    = {2015},
  volume  = {574},
  pages   = {86-91}
}
@inproceedings{sterling:2021:normalization,
  url       = {https://doi.org/10.1109%2Flics52264.2021.9470719},
  year      = 2021,
  month     = 6,
  publisher = {{IEEE}},
  author    = {Jonathan Sterling and Carlo Angiuli},
  title     = {Normalization for Cubical Type Theory},
  booktitle = {2021 36th Annual {ACM}/{IEEE} Symposium on Logic in Computer Science ({LICS})}
}
@misc{amelia:2023:1lab,
  author       = {1Lab contributors},
  howpublished = {\url{https://1lab.dev}},
  title        = {1Lab: A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory},
  year         = {2023}
}
@inproceedings{sterling:2019:xtt,
  author    = {Jonathan Sterling and Carlo Angiuli and Daniel Gratzer},
  title     = {{Cubical Syntax for Reflection-Free Extensional Equality}},
  booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages     = {31:1--31:25},
  series    = {Leibniz International Proceedings in Informatics (LIPIcs)},
  year      = {2019},
  volume    = {131},
  editor    = {Herman Geuvers},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address   = {Dagstuhl, Germany},
  url       = {http://drops.dagstuhl.de/opus/volltexte/2019/10538}
}
@article{gonthier:2008:fourcolor,
  title   = {Formal proof--the four-color theorem},
  author  = {Gonthier, Georges and others},
  journal = {Notices of the AMS},
  volume  = {55},
  number  = {11},
  pages   = {1382--1393},
  year    = {2008}
}
@unpublished{feferman:2000:predicative,
  title  = {Relationships between Constructive, Predicative and Classical Systems of Analysis},
  author = {Solomon Feferman},
  year   = {2000},
  url    = {http://math.stanford.edu/~feferman/papers/relationships.pdf}
}
@article{leroy:2009:compcert,
  title   = {Formal verification of a realistic compiler},
  author  = {Xavier Leroy},
  journal = {Commun. ACM},
  year    = {2009},
  volume  = {52},
  pages   = {107-115}
}
@book{oliveri:2022:structure,
  editor    = {Gianluigi Oliveri, Claudio Ternullo, Stefano Boscolo},
  publisher = {Springer Cham},
  title     = {Objects, Structures, and Logics},
  year      = {2022}
}
@misc{henry:2019:constructive,
  url       = {https://arxiv.org/abs/1905.06160},
  author    = {Simon Henry},
  title     = {A constructive account of the Kan-Quillen model structure and of Kan's Ex$^{\infty}$ functor},
  publisher = {arXiv},
  year      = {2019}
}
@article{huber:2018:canonicity,
  doi     = {10.1007/s10817-018-9469-1},
  journal = {J Autom Reasoning},
  author  = {Simon Huber},
  title   = {Canonicity for Cubical Type Theory},
  year    = {2018}
}
@article{cartmell:1986:contextualcat,
  title   = {Generalised algebraic theories and contextual categories},
  journal = {Annals of Pure and Applied Logic},
  volume  = {32},
  pages   = {209-243},
  year    = {1986},
  issn    = {0168-0072},
  doi     = {https://doi.org/10.1016/0168-0072(86)90053-9},
  author  = {John Cartmell}
}
@inproceedings{hofmann:1995:lccccoh,
  author    = {Martin Hofmann},
  editor    = {Leszek Pacholski and Jerzy Tiuryn},
  title     = {On the interpretation of type theory in locally cartesian closed categories},
  booktitle = {Computer Science Logic},
  year      = {1995},
  publisher = {Springer Berlin Heidelberg},
  address   = {Berlin, Heidelberg},
  pages     = {427--441}
}
@misc{uemura:2019:general,
  url       = {https://arxiv.org/abs/1904.04097},
  author    = {Uemura, Taichi},
  title     = {A General Framework for the Semantics of Type Theory},
  publisher = {arXiv},
  year      = {2019}
}
@article{awodey:2018:natural,
  title     = {Natural models of homotopy type theory},
  volume    = {28},
  doi       = {10.1017/S0960129516000268},
  number    = {2},
  journal   = {Mathematical Structures in Computer Science},
  publisher = {Cambridge University Press},
  author    = {Steve Awodey},
  year      = {2018},
  pages     = {241–286}
}
@article{curien:2014:revisit,
  title   = {Revisiting the categorical interpretation of dependent type theory},
  journal = {Theoretical Computer Science},
  volume  = {546},
  pages   = {99-119},
  year    = {2014},
  issn    = {0304-3975},
  doi     = {https://doi.org/10.1016/j.tcs.2014.03.003},
  author  = {Pierre-Louis Curien and Richard Garner and Martin Hofmann}
}
@article{jacobs:1993:comprehensioncat,
  title   = {Comprehension Categories and the Semantics of Type Dependency},
  author  = {Bart Jacobs},
  journal = {Theor. Comput. Sci.},
  year    = {1993},
  volume  = {107},
  pages   = {169-207}
}
@article{castellan:2019:cwf,
  title   = {Categories with Families: Unityped, Simply Typed, and Dependently Typed},
  author  = {Simon Castellan and Pierre Clairambault and Peter Dybjer},
  journal = {ArXiv},
  year    = {2019},
  volume  = {abs/1904.00827}
}
@misc{sterling:2023:geometry,
  title         = {Towards a geometry for syntax},
  author        = {Jonathan Sterling},
  year          = {2023},
  eprint        = {2307.09497},
  archiveprefix = {arXiv},
  primaryclass  = {cs.LO}
}
@article{curien:1993:coherence,
  author     = {Pierre--Louis Curien},
  title      = {Substitution up to Isomorphism},
  year       = {1993},
  issue_date = {Sept./Oct. 1993},
  publisher  = {IOS Press},
  address    = {NLD},
  volume     = {19},
  number     = {1–2},
  issn       = {0169-2968},
  journal    = {Fundamenta Informaticae},
  month      = {9},
  pages      = {51–85},
  numpages   = {35}
}
@article{clairambault:2014:biequivalence,
  year      = 2014,
  month     = {4},
  publisher = {Cambridge University Press ({CUP})},
  volume    = {24},
  number    = {6},
  author    = {Pierre Clairambault and Peter Dybjer},
  title     = {The biequivalence of locally cartesian closed categories and Martin-Löf type theories},
  journal   = {Mathematical Structures in Computer Science}
}
@phdthesis{newstead:2018:natmod-poly,
  author = {Clive Newstead},
  school = {Carnegie Mellon University},
  title  = {Algebraic models of dependent type theory},
  year   = {2018},
  url    = {https://arxiv.org/abs/2103.06155}
}
@inproceedings{dybjer:1995:internal,
  title     = {Internal Type Theory},
  author    = {Peter Dybjer},
  booktitle = {Types for Proofs and Programs},
  year      = {1995}
}
@article{lumsdaine:2015:universes,
  year      = 2015,
  month     = {7},
  publisher = {Association for Computing Machinery ({ACM})},
  volume    = {16},
  number    = {3},
  pages     = {1--31},
  author    = {Peter Lefanu Lumsdaine and Michael A. Warren},
  title     = {The Local Universes Model},
  journal   = {{ACM} Transactions on Computational Logic}
}
@phdthesis{ullrich:2023:frontend,
  author    = {Sebastian Andreas Ullrich},
  year      = {2023},
  title     = {An Extensible Theorem Proving Frontend},
  doi       = {10.5445/IR/1000161074},
  publisher = {{Karlsruher Institut für Technologie (KIT)}},
  keywords  = {interactive theorem proving, Lean, macros, functional programming},
  pagetotal = {243},
  school    = {Karlsruher Institut für Technologie (KIT)},
  language  = {english}
}
@misc{yang:2023:leandojo,
  title         = {LeanDojo: Theorem Proving with Retrieval-Augmented Language Models},
  author        = {Kaiyu Yang and Aidan M. Swope and Alex Gu and Rahul Chalamala and Peiyang Song and Shixing Yu and Saad Godil and Ryan Prenger and Anima Anandkumar},
  year          = {2023},
  eprint        = {2306.15626},
  archiveprefix = {arXiv},
  primaryclass  = {cs.LG}
}
@misc{gratzer:2021:syntactic,
  title         = {Syntactic categories for dependent type theory: sketching and adequacy},
  author        = {Daniel Gratzer and Jonathan Sterling},
  year          = {2021},
  eprint        = {2012.10783},
  archiveprefix = {arXiv},
  primaryclass  = {cs.LO}
}