types.bib

@string{acm = "Association for Computing Machinery"}
@string{entcs = "Electronic Notes in Theoretical Computer Science"}
@string{ieee = "IEEE Computer Society"}
@string{jfp = "Journal of Functional Programming"}
@string{lmcs = "Logical Methods in Computer Science"}
@string{mscs = "Mathematical Structures in Computer Science"}
@string{tac = "Theory and Applications of Categories"}
@string{tcs = "Theoretical Computer Science"}
@string{tocl = "ACM Transactions on Computational Logic"}

@proceedings{lics:1996,
  booktitle = {Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science},
  date = {1996},
  isbn = {978-0-8186-7463-1},
  publisher = ieee,
  series = {LICS '96},
}

@proceedings{lics:1999,
  booktitle = {Proceedings of the 14th Annual IEEE {S}ymposium on {L}ogic in {C}omputer {S}cience},
  date = {1999},
  isbn = {0-7695-0158-3},
  location = {Trento},
  publisher = {IEEE Computer Soc., Los Alamitos, CA},
  series = {LICS '99},
}

@proceedings{lics:2008,
  booktitle = {Proceedings of the 23rd Annual IEEE Symposium on Logic in Computer Science},
  date = {2008},
  location = {Pittsburgh, PA, USA},
  publisher = ieee,
  series = {LICS '08},
}

@proceedings{popl:2009,
  booktitle = {Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  date = {2009},
  issn = {9781605583792},
  location = {Savannah, GA, USA},
  publisher = acm,
  series = {POPL '09},
}

@proceedings{icfp:2013,
  booktitle = {Proceedings of the 18th Annual ACM SIGPLAN International Conference on Functional Programming},
  date = {2013},
  isbn = {978-1-4503-2326-0},
  location = {Boston, Massachusetts, USA},
  publisher = acm,
  series = {ICFP '13},
}

@proceedings{popl:2013,
  editor = {Giacobazzi, Roberto and Cousot, Radhia},
  booktitle = {Proceedings of the 40th Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages},
  date = {2013},
  isbn = {978-1-4503-1832-7},
  location = {Rome, Italy},
  publisher = acm,
  series = {POPL '13},
}

@proceedings{popl:2014,
  booktitle = {Proceedings of the 41st Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages},
  date = {2014},
  isbn = {978-1-4503-2544-8},
  location = {San Diego, California, USA},
  publisher = acm,
  series = {POPL '14},
}

@proceedings{icfp:2014,
  booktitle = {Proceedings of the 19th {ACM} {SIGPLAN} International Conference on Functional Programming},
  date = {2014},
  isbn = {978-1-4503-2873-9},
  location = {Gothenburg, Sweden},
  publisher = acm,
  series = {ICFP '14},
}

@proceedings{popl:2015,
  booktitle = {Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  date = {2015},
  isbn = {978-1-4503-3300-9},
  location = {Mumbai, India},
  publisher = acm,
  series = {POPL '15},
}

@proceedings{fossacs:2015,
  editor = {Pitts, Andrew},
  booktitle = {18th International Conference on Foundations of Software Science and Computation Structures},
  date = {2015},
  isbn = {978-3-662-46678-0},
  location = {Berlin, Heidelberg},
  publisher = {Springer Berlin Heidelberg},
  series = {FOSSACS '15},
}

@proceedings{types:2015,
  editor = {Uustalu, Tarmo},
  booktitle = {21st International Conference on Types for Proofs and Programs},
  date = {2015},
  isbn = {978-3-95977-030-9},
  issn = {1868-8969},
  location = {Tallinn, Estonia},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  series = {TYPES '15},
  volume = {69},
}

@proceedings{lics:2016,
  booktitle = {Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science},
  date = {2016},
  isbn = {978-1-4503-4391-6},
  location = {New York, NY, USA},
  publisher = acm,
  series = {LICS '16},
}

@proceedings{fscd:2017,
  editor = {Miller, Dale},
  booktitle = {2nd International Conference on Formal Structures for Computation and Deduction},
  date = {2017},
  isbn = {978-3-95977-047-7},
  issn = {1868-8969},
  location = {Dagstuhl, Germany},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  series = {FSCD '17},
  volume = {84},
}

@proceedings{types:2017,
  editor = {Abel, Andreas and Forsberg, Fredrik Nordvall and Kaposi, Ambrus},
  booktitle = {23rd International Conference on Types for Proofs and Programs},
  date = {2017},
  isbn = {978-3-95977-071-2},
  issn = {1868-8969},
  location = {Dagstuhl, Germany},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  series = {TYPES '17},
  volume = {104},
}

@proceedings{fscd:2018,
  booktitle = {3rd International Conference on Formal Structures for Computation and Deduction},
  date = {2018},
  isbn = {978-3-95977-077-4},
  location = {Oxford, {UK}},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  series = {FSCD '18},
}

@proceedings{fossacs:2018,
  booktitle = {21st International Conference on Foundations of Software Science and Computation Structures},
  date = {2018},
  isbn = {978-3-319-89366-2},
  publisher = {Springer International Publishing},
  series = {FOSSACS '18},
  volume = {10803},
}

@proceedings{lics:2018,
  booktitle = {Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science},
  date = {2018},
  isbn = {978-1-4503-5583-4},
  location = {Oxford, United Kingdom},
  publisher = acm,
  series = {LICS '18},
}

@proceedings{lics:2019,
  booktitle = {Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science},
  date = {2019},
  isbn = {978-1-7281-3608-0},
  location = {Vancouver, Canada},
  publisher = acm,
  series = {LICS '19},
}

@proceedings{icfp:2019,
  booktitle = {Proceedings of the 24th ACM SIGPLAN International Conference on Functional Programming},
  date = {2019},
  issn = {2475-1421},
  location = {Boston, Massachusetts, USA},
  publisher = acm,
  series = {ICFP '19},
}

@proceedings{types:2019,
  editor = {Bezem, Marc and Mahboubi, Assia},
  booktitle = {Proceedings of the 25th International Conference on Types for Proofs and Programs},
  date = {2020},
  isbn = {978-3-95977-158-0},
  issn = {1868-8969},
  location = {Dagstuhl, Germany},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum f\"{u}r Informatik},
  series = {TYPES '19},
  volume = {175},
}

@proceedings{icfp:2020,
  booktitle = {Proceedings of the 25th ACM SIGPLAN International Conference on Functional Programming},
  date = {2020},
  location = {Jersey City, USA},
  publisher = acm,
  series = {ICFP '20},
}

@proceedings{lics:2020,
  booktitle = {Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science},
  date = {2020},
  isbn = {978-1-4503-7104-9},
  location = {Saarbr\"{u}cken, Germany},
  publisher = acm,
  series = {LICS '20},
}

@proceedings{lics:2022,
  booktitle = {Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science},
  date = {2022},
  isbn = {978-1-4503-9351-5},
  location = {Haifa, Israel},
  publisher = acm,
  series = {LICS '22},
}

@phdthesis{abel:thesis,
  title = {{A Polymorphic Lambda-Calculus with Sized Higher-Order Types}},
  author = {Abel, Andreas},
  url = {http://www2.tcs.ifi.lmu.de/~abel/diss.pdf},
  date = {2006-06},
}

@article{abel:polarised-subtyping,
  title = {Polarised subtyping for sized types},
  author = {Abel, Andreas},
  date = {2008},
  doi = {10.1017/S0960129508006853},
  journaltitle = mscs,
  number = {5},
  pages = {797--822},
  publisher = {Cambridge University Press},
  volume = {18},
}

@inproceedings{abel:700-modal,
  title = {The Next 700 Modal Type Assignment Systems},
  author = {Abel, Andreas},
  url = {http://www2.tcs.ifi.lmu.de/~abel/types15.pdf},
  crossref = {types:2015},
}

@inproceedings{abel-bernardy:unified-modalities,
  title = {A Unified View of Modalities in Type Systems},
  author = {Abel, Andreas and Bernardy, Jean-Philippe},
  crossref = {icfp:2020},
  doi = {10.1145/3408972},
}

@article{aov:conversion,
  title = {Decidability of conversion for type theory in type theory},
  author = {Abel, Andreas and \"{O}hman, Joakim and Vezzosi, Andrea},
  date = {2017-12},
  doi = {10.1145/3158111},
  journaltitle = {Proc. ACM Program. Lang.},
  location = {New York, NY, USA},
  number = {POPL},
  publisher = acm,
  volume = {2},
}

@inproceedings{copatterns,
  title = {Copatterns: Programming Infinite Structures by Observations},
  author = {Abel, Andreas and Pientka, Brigitte and Thibodeau, David and Setzer, Anton},
  crossref = {popl:2013},
  date = {2013},
  doi = {10.1145/2429069.2429075},
  pages = {27--38},
}

@inproceedings{linton:finiteness1,
  title = {Finiteness and decidability},
  author = {Acu\~{n}a-Ortega, O. and Linton, F. E. J.},
  booktitle = {Applications of sheaves ({P}roc. {R}es. {S}ympos. {A}ppl. {S}heaf {T}heory to {L}ogic, {A}lgebra and {A}nal., {U}niv. {D}urham, {D}urham, 1977)},
  date = {1979},
  doi = {10.1007/BFb0061813},
  pages = {80--100},
  publisher = {Springer, Berlin},
  series = {Lecture Notes in Math.},
  volume = {753},
}

@article{ar:how-nice,
  title = {How nice are free completions of categories?},
  author = {Ad\'{a}mek, Ji\v{r}\'i and Rosick\'{y}, Ji\v{r}\'i},
  date = {2020},
  doi = {10.1016/j.topol.2019.106972},
  issn = {0166-8641},
  journaltitle = {Topology and its Applications},
  pages = {106972,24},
  volume = {273},
}

@inbook{aln:comparing-frameworks,
  title = {Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories},
  author = {Ahrens, Benedikt and Lumsdaine, Peter LeFanu and North, Paige Randall},
  booktitle = {Programming Languages and Systems},
  date = {2024-10},
  doi = {10.1007/978-981-97-8943-6_1},
  isbn = {978-981-9789-43-6},
  issn = {1611-3349},
  pages = {3--22},
  publisher = {Springer Nature Singapore},
}

@online{univalence-principle,
  title = {The Univalence Principle},
  author = {Ahrens, Benedikt and North, Paige Randall and Shulman, Michael and Tsementzis, Dimitris},
  date = {2021},
  eprint = {2102.06275},
  eprintclass = {math.CT},
  eprinttype = {arXiv},
}

@inproceedings{amdr:constructive-s4,
  title = {Categorical and {K}ripke semantics for constructive {S}4 modal logic},
  author = {Alechina, Natasha and Mendler, Michael and de Paiva, Valeria and Ritter, Eike},
  booktitle = {Computer Science Logic},
  date = {2001},
  doi = {10.1007/3-540-44802-0_21},
  pages = {292--307},
  publisher = {Springer, Berlin},
  series = {Lecture Notes in Computer Science},
  volume = {2142},
}

@inproceedings{allais:leftovers,
  title = {Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic},
  author = {Allais, Guillaume},
  crossref = {types:2017},
  doi = {10.4230/LIPIcs.TYPES.2017.1},
  pages = {1:1--1:22},
}

@inproceedings{qiits,
  title = {Quotient Inductive-Inductive Types},
  author = {Altenkirch, Thorsten and Capriotti, Paolo and Dijkstra, Gabe and Kraus, Nicolai and Nordvall Forsberg, Fredrik},
  crossref = {fossacs:2018},
  doi = {10.1007/978-3-319-89366-2_16},
  pages = {293--310},
}

@incollection{ack:hott-strict-equality,
  title = {Extending homotopy type theory with strict equality},
  author = {Altenkirch, Thorsten and Capriotti, Paolo and Kraus, Nicolai},
  booktitle = {Computer Science Logic},
  date = {2016},
  doi = {10.4230/LIPIcs.CSL.2016.21},
  pages = {Art. No. 21,17},
  publisher = {Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern},
  series = {LIPIcs. Leibniz Int. Proc. Inform.},
  volume = {62},
}

@inproceedings{altenkirch-kaposi:without-interval,
  title = {{Towards a Cubical Type Theory without an Interval}},
  author = {Altenkirch, Thorsten and Kaposi, Ambrus},
  editor = {Uustalu, Tarmo},
  booktitle = {21st International Conference on Types for Proofs and Programs (TYPES 2015)},
  date = {2018},
  doi = {10.4230/LIPIcs.TYPES.2015.3},
  isbn = {978-3-95977-030-9},
  issn = {1868-8969},
  location = {Dagstuhl, Germany},
  pages = {3:1--3:27},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  volume = {69},
}

@article{ABG,
  title = {Parametrized Spectra, Multiplicative {T}hom Spectra and the Twisted {U}mkehr Map},
  author = {Ando, Matthew and Blumberg, Andrew and Gepner, David},
  date = {2018-12},
  doi = {10.2140/gt.2018.22.3761},
  issn = {1465-3060},
  journaltitle = {Geometry \& Topology},
  number = {7},
  pages = {3761--3825},
  volume = {22},
}

@article{abghr:thom-oocat,
  title = {An {$\infty$}-categorical approach to {$R$}-line bundles, {$R$}-module {T}hom spectra, and twisted {$R$}-homology},
  author = {Ando, Matthew and Blumberg, Andrew J. and Gepner, David and Hopkins, Michael J. and Rezk, Charles},
  date = {2014},
  doi = {10.1112/jtopol/jtt035},
  issn = {1753-8416},
  journaltitle = {Journal of Topology},
  number = {3},
  pages = {869--893},
  shorthand = {ABGHR},
  volume = {7},
}

@inproceedings{anel:enveloping-topos,
  title = {Enveloping $\infty$-topoi},
  author = {Anel, Mathieu},
  url = {https://www.youtube.com/watch?v=PpfacHtBX8U},
  booktitle = {{Seminar on Higher Homotopical Structures}},
  date = {2021-04},
}

@unpublished{anel:tt-v-geometry,
  title = {Type Theory v. Geometry},
  author = {Anel, Mathieu},
  url = {http://mathieu.anel.free.fr/mat/doc/Anel-2023-HoTT.pdf},
  date = {2023-05},
  location = {Pittsburgh, PA, USA},
  note = {Talk slides.},
  series = {HoTT2023},
}

@article{abfj:blakers-massey,
  title = {A generalized {B}lakers-{M}assey theorem},
  author = {Anel, Mathieu and Biedermann, Georg and Finster, Eric and Joyal, Andr\'{e}},
  date = {2020},
  doi = {10.1112/topo.12163},
  issn = {1753-8416},
  journaltitle = {Journal of Topology},
  number = {4},
  pages = {1521--1553},
  volume = {13},
}

@incollection{anel-joyal:topo-logie,
  title = {Topo-logie},
  author = {Anel, Mathieu and Joyal, Andr\'{e}},
  editor = {Anel, Mathieu and Catren, Gabriel},
  booktitle = {New Spaces in Mathematics: Formal and Conceptual Reflections},
  chapter = {4},
  date = {2021},
  doi = {10.1017/9781108854429.007},
  pages = {155--257},
  publisher = {Cambridge University Press},
  volume = {1},
}

@online{anel-lejay:exponentiable,
  title = {Exponentiable $\infty$-topoi},
  author = {Anel, Mathieu and Lejay, Damien},
  url = {http://mathieu.anel.free.fr/mat/doc/Anel-Lejay-Exponentiable-topoi.pdf},
  date = {2019},
}

@misc{anel-weinberger:smooth-proper,
  title = {Smooth and Proper Maps},
  author = {Anel, Mathieu and Weinberger, Jonathan},
  date = {2024},
  eprint = {2402.00331},
  eprintclass = {math.CT},
  eprinttype = {arXiv},
}

@phdthesis{angiuli:2019,
  title = {Computational Semantics of Cartesian Cubical Type Theory},
  author = {Angiuli, Carlo},
  url = {http://reports-archive.adm.cs.cmu.edu/anon/2019/abstracts/19-127.html},
  date = {2019},
  institution = {Carnegie Mellon University},
  number = {CMU-CS-19-127},
}

@online{two-level-tt,
  title = {Two-Level Type Theory and Applications},
  author = {Annenkov, Danil and Capriotti, Paolo and Kraus, Nicolai and Sattler, Christian},
  date = {2017},
  eprint = {1705.03307},
  eprintclass = {cs.LO},
  eprinttype = {arXiv},
}

@inproceedings{aq:bi-cut-elimination,
  title = {{LBI} Cut Elimination Proof with {BI-MultiCut}},
  author = {Arisaka, Ryuta and Qin, Shengchao},
  booktitle = {2012 Sixth International Symposium on Theoretical Aspects of Software Engineering},
  date = {2012},
  doi = {10.1109/TASE.2012.30},
  pages = {235--238},
}

@phdthesis{armelin:prog-with-bi,
  title = {Programming with Bunched Implications},
  author = {Armelin, Pablo},
  url = {http://qmro.qmul.ac.uk/xmlui/handle/123456789/4746},
  date = {2002},
  institution = {Queen Mary University of London},
}

@inproceedings{arndt-kapulkin:models,
  title = {Homotopy-Theoretic Models of Type Theory},
  author = {Arndt, Peter and Kapulkin, Krzysztof},
  booktitle = {Typed lambda calculi and applications},
  date = {2011},
  doi = {10.1007/978-3-642-21691-6_7},
  pages = {45--60},
  publisher = {Springer, Heidelberg},
  series = {Lecture Notes in Computer Science},
  volume = {6690},
}

@inproceedings{atkey:resource-separation,
  title = {A {$\lambda$}-Calculus for Resource Separation},
  author = {Atkey, Robert},
  booktitle = {Automata, languages and programming},
  date = {2004},
  doi = {10.1007/978-3-540-27836-8_16},
  pages = {158--170},
  publisher = {Springer, Berlin},
  series = {Lecture Notes in Computer Science},
  volume = {3142},
}

@phdthesis{atkey:thesis,
  title = {Substructural Simple Type Theories for Separation and In-place Update},
  author = {Atkey, Robert},
  url = {http://hdl.handle.net/1842/892},
  date = {2006},
  institution = {University of Edinburgh},
}

@inproceedings{atkey:qtt,
  title = {Syntax and Semantics of Quantitative Type Theory},
  author = {Atkey, Robert},
  crossref = {lics:2018},
  doi = {10.1145/3209108.3209189},
  pages = {56--65},
}

@inproceedings{atkey-wood:context-constrained,
  title = {Context Constrained Computation (Extended Abstract)},
  author = {Atkey, Robert and Wood, James},
  booktitle = {3rd Workshop on Type-Driven Development},
  date = {2018},
  series = {TyDe '18},
}

@article{awodey-warren:id-types,
  title = {Homotopy theoretic models of identity types},
  author = {Awodey, Steve and Warren, Michael A.},
  date = {2009},
  doi = {10.1017/S0305004108001783},
  issn = {0305-0041},
  journaltitle = {Mathematical Proceedings of the Cambridge Philosophical Society},
  number = {1},
  pages = {45--55},
  volume = {146},
}

@techreport{barber:dill,
  title = {Dual Intuitionistic Linear Logic},
  author = {Barber, Andrew},
  url = {https://www.lfcs.inf.ed.ac.uk/reports/96/ECS-LFCS-96-347/},
  date = {1996},
  institution = {University of Edinburgh},
  number = {ECS-LFCS-96-347},
}

@online{barwick-haine:pyknotic,
  title = {Pyknotic objects, I. Basic notions},
  author = {Barwick, Clark and Haine, Peter},
  date = {2019},
  eprint = {1904.09966},
  eprintclass = {math.AG},
  eprinttype = {arXiv},
}

@unpublished{bauer:synthetic-talk,
  title = {Synthetic mathematics with an excursion into computability theory},
  author = {Bauer, Andrej},
  url = {https://math.andrej.com/asset/data/madison-synthetic-computability-talk.pdf},
  date = {2021-02},
  location = {University of Wisconsin},
  note = {Talk slides.},
}

@phdthesis{bean:ribbons,
  title = {Ribbon Proofs - A Proof System for the Logic of Bunched Implications},
  author = {Bean, Julian Michael Lewis},
  url = {http://qmro.qmul.ac.uk/xmlui/handle/123456789/5054},
  date = {2006},
  institution = {Queen Mary University of London},
}

@inproceedings{bbdh:term-calculus-ill,
  title = {A term calculus for {Intuitionistic Linear Logic}},
  author = {Benton, Nick and Bierman, Gavin and de Paiva, Valeria and Hyland, Martin},
  booktitle = {Typed lambda calculi and applications},
  date = {1993},
  doi = {10.1007/BFb0037099},
  location = {{U}trecht},
  pages = {75--90},
  publisher = {Springer, Berlin},
  series = {Lecture Notes in Computer Science},
  volume = {664},
}

@inproceedings{benton-wadler:adjoint,
  title = {Linear logic, monads and the lambda calculus},
  author = {Benton, Nick and Wadler, Philip},
  crossref = {lics:1996},
  doi = {10.1109/LICS.1996.561458},
  pages = {420--431},
}

@inproceedings{bo:strong-update-bunched,
  title = {Strong Update, Disposal, and Encapsulation in Bunched Typing},
  author = {Berdine, Josh and O'Hearn, Peter W.},
  booktitle = {Proceedings of the 22nd Annual Conference on Mathematical Foundations of Programming Semantics},
  date = {2006-01},
  doi = {10.1016/j.entcs.2006.04.006},
  pages = {81--98},
  series = {MFPS XXII},
  volume = {158},
}

@inproceedings{tt-in-color,
  title = {Type-Theory in Color},
  author = {Bernardy, Jean-Philippe and Guilhem, Moulin},
  crossref = {icfp:2013},
  doi = {10.1145/2500365.2500577},
  pages = {61--72},
}

@inproceedings{bch:cubes,
  title = {{A Model of Type Theory in Cubical Sets}},
  author = {Bezem, Marc and Coquand, Thierry and Huber, Simon},
  editor = {Matthes, Ralph and Schubert, Aleksy},
  url = {http://drops.dagstuhl.de/opus/volltexte/2014/4628},
  booktitle = {19th International Conference on Types for Proofs and Programs},
  date = {2014},
  doi = {10.4230/LIPIcs.TYPES.2013.107},
  isbn = {978-3-939897-72-9},
  issn = {1868-8969},
  location = {Dagstuhl, Germany},
  pages = {107--128},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  volume = {26},
}

@article{biermandepaiva00modal,
  title = {On an Intuitionistic Modal Logic},
  author = {Bierman, G. M. and de Paiva, V. C. V.},
  date = {2000},
  doi = {10.1023/A:1005291931660},
  issn = {0039-3215},
  journaltitle = {Studia Logica},
  number = {3},
  pages = {383--416},
  volume = {65},
}

@article{drats,
  title = {Modal dependent type theory and dependent right adjoints},
  author = {Birkedal, Lars and Clouston, Ranald and Mannaa, Bassel and Ejlers M\o{}gelberg, Rasmus and Pitts, Andrew M. and Spitters, Bas},
  date = {2020},
  doi = {10.1017/S0960129519000197},
  journaltitle = mscs,
  number = {2},
  pages = {118--138},
  volume = {30},
}

@incollection{gdtt,
  title = {Guarded dependent type theory with coinductive types},
  author = {Bizjak, Ale\v{s} and Grathwohl, Hans Bugge and Clouston, Ranald and M\o{}gelberg, Rasmus E. and Birkedal, Lars},
  booktitle = {Foundations of software science and computation structures},
  date = {2016},
  doi = {10.1007/978-3-662-49630-5_2},
  pages = {20--35},
  publisher = {Springer, Berlin},
  series = {Lecture Notes in Comput. Sci.},
  volume = {9634},
}

@article{blass-scedrov:classifying,
  title = {Classifying topoi and finite forcing},
  author = {Blass, Andreas and \v{S}\v{c}edrov, Andrej},
  date = {1983},
  doi = {10.1016/0022-4049(83)90085-3},
  issn = {0022-4049},
  journaltitle = {J. Pure Appl. Algebra},
  number = {2},
  pages = {111--140},
  volume = {28},
}

@phdthesis{blechschmidt:thesis,
  title = {Using the internal language of toposes in algebraic geometry},
  author = {Blechschmidt, Ingo},
  date = {2017},
  doi = {10.48550/arXiv.2111.03685},
  institution = {University of Augsburg},
}

@online{blechschmidt:qcoh,
  title = {A general Nullstellensatz for generalized spaces},
  author = {Blechschmidt, Ingo},
  url = {https://rawgit.com/iblech/internal-methods/master/paper-qcoh.pdf},
  date = {2017},
}

@misc{bocquet:rezk-completions,
  title = {Strict Rezk completions of models of HoTT and homotopy canonicity},
  author = {Bocquet, Rafa\"{e}l},
  date = {2023},
  eprint = {2311.05849},
  eprintclass = {math.CT},
  eprinttype = {arXiv},
}

@online{bocque-kovacs:frob-j-from-j,
  title = {Deriving a {Frobenius} variant of {J} from {J}},
  author = {Bocquet, Rafael and Kov\'{a}cs, Andr\'{a}s},
  url = {https://github.com/akaposi/hiit-signatures/blob/master/formalization/FrobeniusJDeriv.agda},
  date = {2019},
}

@thesis{deboer:thesis,
  title = {A Proof and Formalization of the Initiality Conjecture of Dependent Type Theory},
  author = {de Boer, Menno},
  url = {http://su.diva-portal.org/smash/record.jsf?pid=diva2\%3A1431287&dswid=-3494},
  date = {2020},
  institution = {Stockholm University},
  type = {Licentiate Thesis},
}

@article{vbm:combinatorial-pspec,
  title = {Combinatorial parametrised spectra},
  author = {Braunack-Mayer, Vincent},
  date = {2021-04},
  doi = {10.2140/agt.2021.21.801},
  issn = {1472-2747},
  journaltitle = {Algebraic \& Geometric Topology},
  number = {2},
  pages = {801--891},
  volume = {21},
}

@inproceedings{focused-nat-ded,
  title = {Focused Natural Deduction},
  author = {Brock-Nannestad, Taus and Sch\"{u}rmann, Carsten},
  booktitle = {Logic for programming, artificial intelligence, and reasoning},
  date = {2010},
  doi = {10.1007/978-3-642-16242-8_12},
  pages = {157--171},
  publisher = {Springer, Berlin},
  series = {Lecture Notes in Computer Science},
  volume = {6397},
}

@inproceedings{quantitative-coeffect-calculus,
  title = {A Core Quantitative Coeffect Calculus},
  author = {Brunel, Alo\"is and Gaboardi, Marco and Mazza, Damiano and Zdancewic, Steve},
  editor = {Shao, Zhong},
  booktitle = {Programming Languages and Systems},
  date = {2014},
  doi = {10.1007/978-3-642-54833-8_19},
  isbn = {978-3-642-54833-8},
  location = {Berlin, Heidelberg},
  pages = {351--370},
  publisher = {Springer Berlin Heidelberg},
}

@phdthesis{brunerie:thesis,
  title = {On the homotopy groups of spheres in homotopy type theory},
  author = {Brunerie, Guillaume},
  date = {2016},
  eprint = {1606.05916},
  eprintclass = {math.AT},
  eprinttype = {arXiv},
  institution = {Universit\'{e} de Nice},
}

@article{brunerie:james-construction,
  title = {The {J}ames construction and {$\pi_4(\Bbb{S}^3)$} in homotopy type theory},
  author = {Brunerie, Guillaume},
  date = {2019},
  doi = {10.1007/s10817-018-9468-2},
  issn = {0168-7433},
  journaltitle = {J. Automat. Reason.},
  number = {2},
  pages = {255--284},
  volume = {63},
}

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

@online{blm:zcohomology,
  title = {Synthetic Cohomology Theory in {Cubical Agda}},
  author = {Brunerie, Guillaume and Ljungstr\"{o}m, Axel and M\"{o}rtberg, Anders},
  url = {https://staff.math.su.se/anders.mortberg/papers/zcohomology.pdf},
  date = {2021},
}

@inproceedings{buchholtz:toy-models,
  title = {Universes in toy models of spatial type theory},
  author = {Buchholtz, Ulrik},
  url = {https://www.youtube.com/watch?v=KpwFDVMxnsM},
  booktitle = {Workshop on Geometry in Modal Homotopy Type Theory},
  date = {2019},
  location = {Carnegie Mellon University},
}

@incollection{bvr:higher-groups-in-hott,
  title = {Higher groups in homotopy type theory},
  author = {Buchholtz, Ulrik and van Doorn, Floris and Rijke, Egbert},
  crossref = {lics:2018},
  doi = {10.1145/3209108.3209150},
}

@article{buchholtz-favonia:cellular-cohomology,
  title = {Cellular Cohomology in {Homotopy Type Theory}},
  author = {Buchholtz, Ulrik and Hou, Kuen-Bang},
  date = {2020-06},
  doi = {10.23638/LMCS-16(2:7)2020},
  issue = {2},
  journaltitle = lmcs,
  volume = {16},
}

@incollection{buchholtz-morehouse:cubes,
  title = {Varieties of cubical sets},
  author = {Buchholtz, Ulrik and Morehouse, Edward},
  booktitle = {Relational and algebraic methods in computer science},
  date = {2017},
  doi = {10.1007/978-3-319-57418-9_5},
  pages = {77--92},
  publisher = {Springer, Cham},
  series = {Lecture Notes in Comput. Sci.},
  volume = {10226},
}

@article{buchholtz-rijke:cayley-dickson,
  title = {The {C}ayley-{D}ickson construction in homotopy type theory},
  author = {Buchholtz, Ulrik and Rijke, Egbert},
  date = {2018},
  doi = {10.31197/atnaa.375870},
  journaltitle = {High. Struct.},
  number = {1},
  pages = {30--41},
  volume = {2},
}

@online{weinberger-buchholtz:synthetic-cats,
  title = {Synthetic fibered $(\infty,1)$-category theory},
  author = {Buchholtz, Ulrik and Weinberger, Jonathan},
  date = {2021},
  eprint = {2105.01724},
  eprintclass = {math.CT},
  eprinttype = {arXiv},
}

@book{bgs:sdt,
  title = {Synthetic differential topology},
  author = {Bunge, Marta and Gago, Felipe and San Luis, Ana Mar\'ia},
  date = {2018},
  doi = {10.1017/9781108553490},
  isbn = {978-1-108-44723-2},
  pages = {ix+223},
  publisher = {Cambridge University Press, Cambridge},
  series = {London Mathematical Society Lecture Note Series},
  volume = {448},
}

@book{caramello:book,
  title = {Theories, Sites, Toposes},
  author = {Caramello, Olivia},
  date = {2018},
  isbn = {978-0-19-875891-4},
  note = {Relating and studying mathematical theories through topos-theoretic `bridges'},
  pages = {xii+368},
  publisher = {Oxford University Press, Oxford},
}

@article{carchedi-roytenberg:superalgebra,
  title = {On theories of superalgebras of differentiable functions},
  author = {Carchedi, David and Roytenberg, Dmitry},
  url = {http://www.tac.mta.ca/tac/volumes/28/30/28-30abs.html},
  date = {2013},
  journaltitle = tac,
  pages = {No. 30,1022--1098},
  volume = {28},
}

@mastersthesis{cavallo:cohomology,
  title = {Synthetic Cohomology in {Homotopy Type Theory}},
  author = {Cavallo, Evan},
  url = {https://staff.math.su.se/evan.cavallo/works/thesis15.pdf},
  date = {2015-12},
  institution = {Carnegie Mellon University},
}

@phdthesis{cavallo:thesis,
  title = {Higher Inductive Types and Internal Parametricity for Cubical Type Theory},
  author = {Cavallo, Evan},
  date = {2021},
  doi = {10.1184/R1/14555691},
  institution = {Carnegie Mellon University},
  number = {CMU-CS-21-100},
}

@inproceedings{cavallo-harper:parametricity-for-ctt,
  title = {{Internal Parametricity for Cubical Type Theory}},
  author = {Cavallo, Evan and Harper, Robert},
  booktitle = {28th EACSL Annual Conference on Computer Science Logic 2020)},
  date = {2020},
  doi = {10.4230/LIPIcs.CSL.2020.13},
  isbn = {978-3-95977-132-0},
  issn = {1868-8969},
  location = {Dagstuhl, Germany},
  pages = {13:1--13:17},
  series = {CSL '20},
  volume = {152},
}

@incollection{cms:unifying-cubical,
  title = {Unifying cubical models of univalent type theory},
  author = {Cavallo, Evan and M\"{o}rtberg, Anders and Swan, Andrew W.},
  booktitle = {28th {EACSL} {A}nnual {C}onference on {C}omputer {S}cience {L}ogic},
  date = {2020},
  doi = {10.4230/LIPIcs.CSL.2020.14},
  pages = {Art. No. 14,17},
  publisher = {Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern},
  series = {LIPIcs. Leibniz Int. Proc. Inform.},
  volume = {152},
}

@inproceedings{cervesato-pfenning:lin-lf,
  title = {A Linear Logical Framework},
  author = {Cervesato, Iliano and Pfenning, Frank},
  crossref = {lics:1996},
  doi = {10.1006/inco.2001.2951},
  pages = {19--75},
}

@misc{chan-weirich:universe-levels,
  title = {Bounded First-Class Universe Levels in Dependent Type Theory},
  author = {Chan, Jonathan and Weirich, Stephanie},
  date = {2025},
  eprint = {2502.20485},
  eprintclass = {cs.PL},
  eprinttype = {arXiv},
}

@inproceedings{cheney:simple,
  title = {A Simple Nominal Type Theory},
  author = {Cheney, James},
  booktitle = {Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice (LFMTP 2008)},
  date = {2009},
  doi = {10.1016/j.entcs.2008.12.115},
  pages = {37--52},
  volume = {228},
}

@article{cheney:dntt,
  title = {A dependent nominal type theory},
  author = {Cheney, James},
  date = {2012},
  doi = {10.2168/LMCS-8(1:8)2012},
  journaltitle = lmcs,
  number = {1},
  pages = {1:08,29},
  volume = {8},
}

@article{cch:sag,
  title = {A foundation for synthetic algebraic geometry},
  author = {Cherubini, Felix and Coquand, Thierry and Hutzler, Matthias},
  date = {2024},
  doi = {10.1017/S0960129524000239},
  issn = {0960-1295},
  journaltitle = {Math. Structures Comput. Sci.},
  number = {9},
  pages = {1008--1053},
  volume = {34},
}

@misc{cchw:projective-space-sag,
  title = {Projective Space in Synthetic Algebraic Geometry},
  author = {Cherubini, Felix and Coquand, Thierry and Hutzler, Matthias and W\"{a}rn, David},
  date = {2024},
  eprint = {2405.13916},
  eprintclass = {math.AG},
  eprinttype = {arXiv},
}

@article{cors:localization-in-hott,
  title = {Localization in homotopy type theory},
  author = {Christensen, J. Daniel and Opie, Morgan and Rijke, Egbert and Scoccola, Luis},
  url = {https://higher-structures.math.cas.cz/api/files/issues/Vol4Iss1/ChrOpiRijSco},
  date = {2020},
  journaltitle = {Higher Structures},
  number = {1},
  pages = {1--32},
  volume = {4},
}

@article{clairambault-dybjer:bieq,
  title = {The biequivalence of locally cartesian closed categories and {M}artin-{L}\"{o}f type theories},
  author = {Clairambault, Pierre and Dybjer, Peter},
  date = {2014},
  doi = {10.1017/S0960129513000881},
  issn = {0960-1295},
  journaltitle = mscs,
  number = {6},
  pages = {e240606},
  volume = {24},
}

@misc{clausen-sholze:condensed,
  title = {Lectures on Condensed Mathematics},
  author = {Clausen, Dustin and Scholze, Peter},
  url = {https://www.math.uni-bonn.de/people/scholze/Condensed.pdf},
  date = {2019},
}

@inproceedings{clouston:fitch-style,
  title = {Fitch-Style Modal Lambda Calculi},
  author = {Clouston, Ranald},
  booktitle = {Foundations of software science and computation structures},
  date = {2018},
  doi = {10.1007/978-3-319-89366-2_14},
  pages = {258--275},
  publisher = {Springer, Cham},
  series = {Lecture Notes in Comput. Sci.},
  volume = {10803},
}

@inproceedings{clouston:fitch,
  title = {Fitch-Style Modal Lambda Calculi},
  author = {Clouston, Ranald},
  crossref = {fossacs:2018},
  doi = {10.1007/978-3-319-89366-2_14},
  pages = {258--275},
}

@article{cdp:without-k,
  title = {Eliminating dependent pattern matching without {K}},
  author = {Cockx, Jesper and Devriese, Dominique and Piessens, Frank},
  date = {2016},
  doi = {10.1017/S0956796816000174},
  pages = {e16},
  publisher = {Cambridge University Press},
  volume = {26},
}

@inproceedings{cp:bunching-regions,
  title = {Bunching for Regions and Locations},
  author = {Collinson, Matthew and Pym, David},
  booktitle = {Proceedings of the 22nd Annual Conference on Mathematical Foundations of Programming Semantics},
  date = {2006-05},
  doi = {10.1016/j.entcs.2006.04.010},
  number = {158},
  pages = {171--197},
  series = {MFPS XXII},
}

@article{cpr:bunched-poly,
  title = {Bunched polymorphism},
  author = {Collinson, Matthew and Pym, David and Robinson, Edmund},
  date = {2008},
  doi = {10.1017/S0960129508007159},
  issn = {0960-1295},
  journaltitle = mscs,
  number = {6},
  pages = {1091--1132},
  volume = {18},
}

@inproceedings{coquand:dep-pattern,
  title = {Pattern Matching with Dependent Types},
  author = {Coquand, Thierry},
  url = {https://wonks.github.io/type-theory-reading-group/papers/proc92-coquand.pdf},
  booktitle = {Types for Proofs and Programs},
  date = {1992},
}

@incollection{chs:canonicity-conference,
  title = {Homotopy canonicity for cubical type theory},
  author = {Coquand, Thierry and Huber, Simon and Sattler, Christian},
  booktitle = {4th {I}nternational {C}onference on {F}ormal {S}tructures for {C}omputation and {D}eduction},
  date = {2019},
  pages = {Art. No. 11,23},
  publisher = {Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern},
  series = {LIPIcs. Leibniz Int. Proc. Inform.},
  volume = {131},
}

@article{chs:canonicity,
  title = {Canonicity and homotopy canonicity for cubical type theory},
  author = {Coquand, Thierry and Huber, Simon and Sattler, Christian},
  date = {2022},
  doi = {10.46298/lmcs-18(1:28)2022},
  journaltitle = {Log. Methods Comput. Sci.},
  number = {1},
  pages = {Paper No. 28,35},
  volume = {18},
}

@online{crs:sheaf-models,
  title = {Constructive sheaf models of type theory},
  author = {Coquand, Thierry and Ruch, Fabian and Sattler, Christian},
  date = {2020},
  eprint = {1912.10407},
  eprintclass = {math.LO},
  eprinttype = {arXiv},
}

@incollection{day:convolution,
  title = {On closed categories of functors},
  author = {Day, Brian},
  booktitle = {Reports of the {M}idwest {C}ategory {S}eminar, {IV}},
  date = {1970},
  doi = {10.1007/BFb0060438},
  pages = {1--38},
  publisher = {Springer, Berlin},
  series = {Lecture Notes in Mathematics, Vol. 137},
}

@inproceedings{dybjer:cwf,
  title = {Internal type theory},
  author = {Dybjer, Peter},
  booktitle = {Types for Proofs and Programs},
  date = {1996},
  doi = {10.1007/3-540-61780-9_66},
  isbn = {978-3-540-70722-6},
  location = {Torino},
  pages = {120--134},
  publisher = {Springer, Berlin},
  series = {Lecture Notes in Computer Science},
  volume = {1158},
}

@article{escardo:extended-nats,
  title = {Infinite sets that satisfy the principle of omniscience in any variety of constructive mathematics},
  author = {Escard\'{o}, Mart\'in H.},
  date = {2013},
  doi = {10.2178/jsl.7803040},
  issn = {0022-4812},
  journaltitle = {The Journal of Symbolic Logic},
  number = {3},
  pages = {764--784},
  volume = {78},
}

@article{fhm:left-and-right,
  title = {Isomorphisms between left and right adjoints},
  author = {Fausk, H. and Hu, P. and May, J. P.},
  url = {https://eudml.org/doc/123681},
  date = {2003},
  issn = {1201-561X},
  journaltitle = tac,
  pages = {No. 4,107--131 (electronic)},
  volume = {11},
}

@inproceedings{finster:ha-talk,
  title = {Towards higher universal algebra in type theory},
  author = {Finster, Eric},
  url = {https://www.youtube.com/watch?v=hlCVHVtAlqQ},
  booktitle = {{Homotopy Type Theory Electronic Seminar Talks}},
  date = {2018},
}

@article{fiore:semantic-nbe,
  title = {Semantic analysis of normalisation by evaluation for typed lambda calculus},
  author = {Fiore, Marcelo},
  date = {2022},
  doi = {10.1017/s0960129522000263},
  issn = {0960-1295},
  journaltitle = {Math. Structures Comput. Sci.},
  number = {8},
  pages = {1028--1065},
  volume = {32},
}

@incollection{fpt:abstract-syntax,
  title = {Abstract syntax and variable binding (extended abstract)},
  author = {Fiore, Marcelo and Plotkin, Gordon and Turi, Daniele},
  crossref = {lics:1999},
  doi = {10.1109/LICS.1999.782615},
  pages = {193--202},
}

@inproceedings{ft:name-value-passing,
  title = {Semantics of Name and Value Passing},
  author = {Fiore, Marcelo and Turi, Daniele},
  booktitle = {Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science},
  date = {2001},
  doi = {10.1109/LICS.2001.932486},
  location = {USA},
  pages = {93},
  publisher = ieee,
  series = {LICS '01},
}

@mastersthesis{franz:thesis,
  title = {The wedge sum and the smash product in Homotopy Type Theory},
  author = {Franz, Andreas},
  url = {https://www.math.lmu.de/~petrakis/Franz.pdf},
  date = {2017},
  institution = {Ludwig-Maximilians-Universit\"{a}t M\"{u}nchen},
}

@article{bireflectivity,
  title = {Bireflectivity},
  author = {Freyd, P. J. and O'Hearn, P. W. and Power, A. J. and Takeyama, M. and Street, R. and Tennent, R. D.},
  date = {1999},
  doi = {10.1016/S0304-3975(98)00354-5},
  issn = {0304-3975},
  journaltitle = tcs,
  number = {1-2},
  pages = {49--76},
  volume = {228},
}

@online{frumin:semantic-cut-elimination,
  title = {Semantic Cut Elimination for the Logic of Bunched Implications, Formalized in {Coq}},
  author = {Frumin, Dan},
  date = {2021},
  eprint = {2112.05515},
  eprintclass = {cs.LO},
  eprinttype = {arXiv},
  pubstate = {forthcoming},
}

@inproceedings{hott-finite-sets,
  title = {Finite Sets in Homotopy Type Theory},
  author = {Frumin, Dan and Geuvers, Herman and Gondelman, L\'{e}on and Weide, Niels van der},
  booktitle = {Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs},
  date = {2018},
  doi = {10.1145/3167085},
  isbn = {978-1-4503-5586-5},
  location = {Los Angeles, CA, USA},
  pages = {201--214},
  publisher = acm,
  series = {CPP 2018},
}

@inproceedings{pknp:proto-quipper-tutorial,
  title = {A Tutorial Introduction to Quantum Circuit Programming in Dependently Typed Proto-Quipper},
  author = {Fu, Peng and Kishida, Kohei and Ross, Neil J. and Selinger, Peter},
  booktitle = {Reversible Computation},
  date = {2020},
  doi = {10.1007/978-3-030-52482-1_9},
  isbn = {978-3-030-52482-1},
  location = {Cham},
  pages = {153--168},
  publisher = {Springer International Publishing},
}

@inproceedings{pkp:dependent-proto-quipper,
  title = {Linear Dependent Type Theory for Quantum Programming Languages: Extended Abstract},
  author = {Fu, Peng and Kishida, Kohei and Selinger, Peter},
  crossref = {lics:2020},
  doi = {10.1145/3373718.3394765},
  pages = {440--453},
}

@article{gabbay-pitts:nominal,
  title = {A New Approach to Abstract Syntax with Variable Binding},
  author = {Gabbay, Murdoch J. and Pitts, Andrew M.},
  date = {2001-07},
  doi = {10.1007/s001650200016},
  journaltitle = {Formal Aspects of Computing},
  number = {3--5},
  pages = {341--363},
  volume = {13},
}

@article{gambino-garner,
  title = {The identity type weak factorisation system},
  author = {Gambino, Nicola and Garner, Richard},
  date = {2008},
  doi = {10.1016/j.tcs.2008.08.030},
  issn = {0304-3975},
  journaltitle = tcs,
  number = {1},
  pages = {94--109},
  volume = {409},
}

@article{garner-lack:lex-colimits,
  title = {Lex colimits},
  author = {Garner, Richard and Lack, Stephen},
  date = {2012},
  doi = {10.1016/j.jpaa.2012.01.003},
  issn = {0022-4049},
  journaltitle = {J. Pure Appl. Algebra},
  number = {6},
  pages = {1372--1396},
  volume = {216},
}

@article{gepner-kock:univalence,
  title = {Univalence in locally cartesian closed {$\infty$}-categories},
  author = {Gepner, David and Kock, Joachim},
  date = {2017},
  doi = {10.1515/forum-2015-0228},
  issn = {0933-7741},
  journaltitle = {Forum Mathematicum},
  number = {3},
  pages = {617--652},
  volume = {29},
}

@article{girard:ll,
  title = {Linear logic},
  author = {Girard, Jean-Yves},
  date = {1987},
  doi = {10.1016/0304-3975(87)90045-4},
  issn = {0304-3975},
  journaltitle = tcs,
  number = {1},
  pages = {101},
  volume = {50},
}

@article{girard-scedrov-scott:bounded-ll,
  title = {Bounded linear logic: a modular approach to polynomial-time computability},
  author = {Girard, Jean-Yves and Scedrov, Andre and Scott, Philip J.},
  date = {1992},
  doi = {10.1016/0304-3975(92)90386-T},
  issn = {0304-3975},
  journaltitle = tcs,
  number = {1},
  pages = {1--66},
  volume = {97},
}

@online{graham:homology,
  title = {Synthetic Homology in {Homotopy Type Theory}},
  author = {Graham, Robert},
  date = {2018},
  eprint = {1706.01540},
  eprintclass = {math.LO},
  eprinttype = {arXiv},
}

@online{gratzer:crisp-id-induction,
  title = {Crisp induction for intensional identity types},
  author = {Gratzer, Daniel},
  url = {https://jozefg.github.io/papers/crisp-induction-for-intensional-identity-types.pdf},
  date = {2021},
}

@inproceedings{gratzer:normalization,
  title = {Normalization for multimodal type theory},
  author = {Gratzer, Daniel},
  booktitle = {Proceedings of the 37th {A}nnual {ACM}/{IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience},
  date = {2022},
  doi = {10.1145/3531130.3532398},
  publisher = {ACM, New York},
}

@online{gratzer:adjoint,
  title = {Adjoint Modalities in {MTT}},
  author = {Gratzer, Daniel},
  url = {https://jozefg.github.io/papers/adjoint-modalities-in-mtt.pdf},
  date = {2023},
}

@article{mtt-fitch,
  title = {Modalities and Parametric Adjoints},
  author = {Gratzer, Daniel and Cavallo, Evan and Kavvos, G. A. and Guatto, Adrien and Birkedal, Lars},
  date = {2022-04},
  doi = {10.1145/3514241},
  issn = {1529-3785},
  journaltitle = {ACM Trans. Comput. Logic},
  location = {New York, NY, USA},
  number = {3},
  publisher = acm,
  volume = {23},
}

@article{fitchtt,
  title = {Modalities and Parametric Adjoints},
  author = {Gratzer, Daniel and Cavallo, Evan and Kavvos, G. A. and Guatto, Adrien and Birkedal, Lars},
  date = {2022-04},
  doi = {10.1145/3514241},
  issn = {1529-3785},
  journaltitle = {ACM Trans. Comput. Logic},
  location = {New York, NY, USA},
  number = {3},
  publisher = acm,
  volume = {23},
}

@techreport{mtt:tech-report,
  title = {Type Theory \`{a} la Mode},
  author = {Gratzer, Daniel and Kavvos, G. A. and Nuyts, Andreas and Birkedal, Lars},
  url = {https://jozefg.github.io/papers/type-theory-a-la-mode.pdf},
  date = {2020-04},
}

@inproceedings{mtt,
  title = {Multimodal Dependent Type Theory},
  author = {Gratzer, Daniel and Kavvos, G. A. and Nuyts, Andreas and Birkedal, Lars},
  crossref = {lics:2020},
  doi = {10.1145/3373718.3394736},
  pages = {492--506},
}

@inproceedings{gsb:implementing,
  title = {Implementing a modal dependent type theory},
  author = {Gratzer, Daniel and Sterling, Jonathan and Birkedal, Lars},
  crossref = {icfp:2019},
  doi = {10.1145/3341711},
  pages = {107:1--107:29},
}

@misc{gwb:directed-univalence,
  title = {Directed univalence in simplicial homotopy type theory},
  author = {Gratzer, Daniel and Weinberger, Jonathan and Buchholtz, Ulrik},
  date = {2024},
  eprint = {2407.09146},
  eprintclass = {cs.LO},
  eprinttype = {arXiv},
}

@misc{gwb:yoneda,
  title = {The Yoneda embedding in simplicial type theory},
  author = {Gratzer, Daniel and Weinberger, Jonathan and Buchholtz, Ulrik},
  date = {2025},
  eprint = {2501.13229},
  eprintclass = {cs.LO},
  eprinttype = {arXiv},
}

@article{guglielmi:calc-of-structures,
  title = {A system of interaction and structure},
  author = {Guglielmi, Alessio},
  date = {2007},
  doi = {10.1145/1182613.1182614},
  issn = {1529-3785},
  journaltitle = tocl,
  number = {1},
  pages = {Art. 1,64},
  volume = {8},
}

@inproceedings{hadzihasanovic:smash,
  title = {The {S}mash {P}roduct of {M}onoidal {T}heories},
  author = {Hadzihasanovic, Amar},
  booktitle = {Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science},
  date = {2021},
  doi = {10.1109/LICS52264.2021.9470575},
  isbn = {978-1-6654-4895-6},
  location = {New York, NY, USA},
  publisher = acm,
}

@inproceedings{rlz:pronomial,
  title = {A Pronominal Approach to Binding and Computation},
  author = {Harper, Robert and Licata, Daniel R. and Zeilberger, Noam},
  booktitle = {Typed Lambda Calculi and Applications},
  date = {2009},
  doi = {10.1007/978-3-642-02273-9_2},
}

@phdthesis{henry:2013,
  title = {Classifying Topoi and Preservation of Higher Order Logic by Geometric Morphisms},
  author = {Henry, Shawn J.},
  date = {2013},
  doi = {2027.42/99993},
  institution = {The University of Michigan},
}

@incollection{hofmann:interp,
  title = {Syntax and Semantics of Dependent Types},
  author = {Hofmann, Martin},
  booktitle = {Semantics and Logics of Computation},
  date = {1997},
  doi = {10.1017/CBO9780511526619.004},
  pages = {79--130},
  publisher = {Cambridge University Press},
  volume = {14},
}

@incollection{hofmann:hoas,
  title = {Semantical analysis of higher-order abstract syntax},
  author = {Hofmann, Martin},
  crossref = {lics:1999},
  doi = {10.1109/LICS.1999.782616},
}

@mastersthesis{horsfall:thesis,
  title = {The Logic of Bunched Implications: A Memoir},
  author = {Horsfall, Benjamin Robert},
  url = {http://hdl.handle.net/11343/39480},
  date = {2006},
  institution = {The University of Melbourne},
}

@inproceedings{hfll:blakers-massey,
  title = {A Mechanization of the {Blakers-Massey} Connectivity Theorem in {Homotopy Type Theory}},
  author = {Hou, Kuen-Bang and Finster, Eric and Licata, Daniel R. and Lumsdaine, Peter LeFanu},
  crossref = {lics:2016},
  doi = {10.1145/2933575.2934545},
  pages = {10},
}

@article{hoyois:topoi-param,
  title = {Topoi of parametrized objects},
  author = {Hoyois, Marc},
  url = {http://www.tac.mta.ca/tac/volumes/34/9/34-09abs.html},
  date = {2019},
  journaltitle = tac,
  pages = {Paper No. 9,243--248},
  volume = {34},
}

@misc{hutzler:glued,
  title = {Syntactic presentations for glued toposes and for crystalline toposes},
  author = {Hutzler, Matthias},
  date = {2022},
  eprint = {2206.11244},
  eprintclass = {math.CT},
  eprinttype = {arXiv},
}

@incollection{hyland:sdt,
  title = {First steps in synthetic domain theory},
  author = {Hyland, J. M. E.},
  booktitle = {Category theory ({C}omo, 1990)},
  date = {1991},
  doi = {10.1007/BFb0084217},
  pages = {131--156},
  publisher = {Springer, Berlin},
  series = {Lecture Notes in Math.},
  volume = {1488},
}

@article{fill,
  title = {Full intuitionistic linear logic (extended abstract)},
  author = {Hyland, Martin and de Paiva, Valeria},
  date = {1993},
  doi = {10.1016/0168-0072(93)90146-5},
  issn = {0168-0072},
  journaltitle = {Ann. Pure Appl. Logic},
  number = {3},
  pages = {273--291},
  volume = {64},
}

@inproceedings{isaev:itt-talk,
  title = {Indexed type theories},
  author = {Isaev, Valery},
  url = {https://www.youtube.com/watch?v=PzjmjIlc-kE},
  booktitle = {{Homotopy Type Theory Electronic Seminar Talks}},
  date = {2020},
}

@article{isaev:itt,
  title = {Indexed type theories},
  author = {Isaev, Valery},
  date = {2021},
  doi = {10.1017/S0960129520000092},
  journaltitle = mscs,
  number = {1},
  pages = {3--63},
  volume = {31},
}

@article{ishtiaq-pym:deplin,
  title = {A Relevant Analysis of Natural Deduction},
  author = {Ishtiaq, S. S. and Pym, D. J.},
  date = {1998},
  doi = {10.1093/logcom/8.6.809},
  issn = {0955-792X},
  journaltitle = {Journal of Logic and Computation},
  number = {6},
  pages = {809--838},
  volume = {8},
}

@inproceedings{ishtiaq-pym:kripke-models,
  title = {{Kripke} Resource Models of a Dependently-Typed Bunched {$\lambda$}-Calculus (Extended Abstract)},
  author = {Ishtiaq, Samin and Pym, David J.},
  booktitle = {Computer Science Logic},
  date = {1999},
  doi = {10.1007/3-540-48168-0_17},
  pages = {235--249},
  publisher = {Springer, Berlin},
  series = {Lecture Notes in Computer Science},
  volume = {1683},
}

@article{johnstone:topological-topos,
  title = {On a topological topos},
  author = {Johnstone, P. T.},
  date = {1979},
  doi = {10.1112/plms/s3-38.2.237},
  issn = {0024-6115},
  journaltitle = {Proceedings of the London Mathematical Society. Third Series},
  number = {2},
  pages = {237--271},
  volume = {38},
}

@article{linton:finiteness2,
  title = {Finiteness and decidability. {II}},
  author = {Johnstone, P. T. and Linton, F. E. J.},
  date = {1978},
  doi = {10.1017/S0305004100055043},
  issn = {0305-0041},
  journaltitle = {Math. Proc. Cambridge Philos. Soc.},
  number = {2},
  pages = {207--218},
  volume = {84},
}

@online{joyal:notes,
  title = {Notes on Logoi},
  author = {Joyal, Andr\'{e}},
  url = {http://www.math.uchicago.edu/~may/IMA/JOYAL/Joyal.pdf},
  date = {2008},
}

@article{kapulkin-lumsdaine:simplicial,
  title = {The simplicial model of {Univalent} {Foundations} (after {Voevodsky})},
  author = {Kapulkin, Krzysztof and Lumsdaine, Peter LeFanu},
  date = {2021},
  doi = {10.4171/JEMS/1050},
  issn = {1435-9855},
  journaltitle = {Journal of the European Mathematical Society},
  number = {6},
  pages = {2071--2126},
  volume = {23},
}

@inproceedings{kock-reyes:manifolds,
  title = {Manifolds in formal differential geometry},
  author = {Kock, A. and Reyes, G. E.},
  booktitle = {Applications of sheaves ({P}roc. {R}es. {S}ympos. {A}ppl. {S}heaf {T}heory to {L}ogic, {A}lgebra and {A}nal., {U}niv. {D}urham, {D}urham, 1977)},
  date = {1979},
  pages = {514--533},
  publisher = {Springer, Berlin},
  series = {Lecture Notes in Math.},
  volume = {753},
}

@misc{kock:commutation,
  title = {Commutation Structures},
  author = {Kock, Anders},
  date = {2005},
  eprint = {math/0511040},
  eprintclass = {math.CT},
  eprinttype = {arXiv},
}

@book{kock:sdg,
  title = {Synthetic Differential Geometry},
  author = {Kock, Anders},
  date = {2006},
  doi = {10.1017/CBO9780511550812},
  edition = {2},
  isbn = {978-0-521-68738-6},
  pages = {xii+233},
  publisher = {Cambridge University Press, Cambridge},
  series = {London Mathematical Society Lecture Note Series},
  volume = {333},
}

@online{kock-reyes:differential-equations,
  title = {Fractional Exponent Functors and Categories of Differential Equations},
  author = {Kock, Anders and Reyes, Gonzalo E.},
  url = {https://tildeweb.au.dk/au76680/ODE55.pdf},
  date = {1998},
}

@article{kock-reyes:fractional,
  title = {Aspects of fractional exponent functors},
  author = {Kock, Anders and Reyes, Gonzalo E.},
  url = {http://www.tac.mta.ca/tac/volumes/1999/n10/5-10abs.html},
  date = {1999},
  journaltitle = tac,
  pages = {No. 10,251--265},
  volume = {5},
}

@inproceedings{astra:ss-talk,
  title = {Semi-simplicial types},
  author = {Kolomatskaia, Astra},
  url = {https://www.youtube.com/watch?v=fQv2FpeFxew},
  booktitle = {{Homotopy Type Theory Electronic Seminar Talks}},
  date = {2022},
}

@inproceedings{kovacs-kamposi:qiits,
  title = {Large and infinitary quotient inductive-inductive types},
  author = {Kov\'{a}cs, Andr\'{a}s and Kaposi, Ambrus},
  booktitle = {Proceedings of the 35th {A}nnual {ACM}/{IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS} 2020)},
  date = {2020},
  doi = {10.1145/3373718.3394770},
  pages = {14},
  publisher = {ACM, New York},
}

@online{kraus-sattler:spacediagrams,
  title = {Space-Valued Diagrams, Type-Theoretically (Extended Abstract)},
  author = {Kraus, Nicolai and Sattler, Christian},
  date = {2017},
  eprint = {1704.04543},
  eprintclass = {math.LO},
  eprinttype = {arXiv},
}

@online{krishnaswami:bi,
  title = {A new lambda calculus for bunched implications},
  author = {Krishnaswami, Neel},
  url = {https://semantic-domain.blogspot.com/2011/07/new-lambda-calculus-for-bunched.html},
  date = {2011-07-27},
}

@online{krishnaswami:separation-sequent,
  title = {A Modal Sequent Calculus for Propositional Separation Logic},
  author = {Krishnaswami, Neelakantan R.},
  url = {https://www.cl.cam.ac.uk/~nk480/separation-sequent.pdf},
  booktitle = {Proceedings of the Workshop on Intuitionistic Modal Logic and Applications (IMLA'08)},
  date = {2008-06},
}

@inproceedings{krishnaswami:pattern,
  title = {Focusing on Pattern Matching},
  author = {Krishnaswami, Neelakantan R.},
  crossref = {popl:2009},
  doi = {10.1145/1480881.1480927},
  pages = {366--378},
}

@inproceedings{kpb:lnld,
  title = {Integrating Linear and Dependent Types},
  author = {Krishnaswami, Neelakantan R. and Pradic, Pierre and Benton, Nick},
  crossref = {popl:2015},
  doi = {10.1145/2676726.2676969},
  pages = {17--30},
}

@book{lavendhomme:book,
  title = {Basic concepts of synthetic differential geometry},
  author = {Lavendhomme, Ren\'{e}},
  date = {1996},
  doi = {10.1007/978-1-4757-4588-7},
  isbn = {0-7923-3941-X},
  note = {Translated from the 1987 French original, Revised by the author},
  pages = {xvi+320},
  publisher = {Kluwer Academic Publishers Group, Dordrecht},
  series = {Kluwer Texts in the Mathematical Sciences},
  volume = {13},
}

@incollection{lawvere:quantifiers-sheaves,
  title = {Quantifiers and sheaves},
  author = {Lawvere, F. W.},
  url = {https://github.com/mattearnshaw/lawvere/raw/master/pdfs/1970-quantifiers-and-sheaves.pdf},
  booktitle = {Actes du {C}ongr\`{e}s {I}nternational des {M}ath\'{e}maticiens ({N}ice, 1970), {T}ome 1},
  date = {1971},
  pages = {329--334},
  publisher = {Gauthier-Villars, Paris},
}

@incollection{lawvere:cantor,
  title = {Cohesive toposes and {C}antor's ``lauter {E}insen''},
  author = {Lawvere, F. W.},
  date = {1994},
  doi = {10.1093/philmat/2.1.5},
  issn = {0031-8019},
  journaltitle = {Philos. Math. (3)},
  note = {Categories in the foundations of mathematics and language},
  number = {1},
  pages = {5--15},
  volume = {2},
}

@article{lawvere-menni:internal-choice,
  title = {Internal choice holds in the discrete part of any cohesive topos satisfying stable connected codiscreteness},
  author = {Lawvere, F. W. and Menni, M.},
  url = {http://www.tac.mta.ca/tac/volumes/30/26/30-26abs.html},
  date = {2015},
  journaltitle = {Theory Appl. Categ.},
  pages = {Paper No. 26,909--932},
  volume = {30},
}

@incollection{lawvere:categorical-dynamics,
  title = {Categorical dynamics},
  author = {Lawvere, F. William},
  url = {https://github.com/mattearnshaw/lawvere/raw/master/pdfs/1978-categorical-dynamics.pdf},
  booktitle = {Topos theoretic methods in geometry},
  date = {1979},
  pages = {1--28},
  publisher = {Aarhus Univ., Aarhus},
  series = {Various Publications Series},
  volume = {30},
}

@article{lawvere:towards,
  title = {Toward the description in a smooth topos of the dynamically possible motions and deformations of a continuous body},
  author = {Lawvere, F. William},
  url = {http://www.numdam.org/item/?id=CTGDC_1980__21_4_377_0},
  date = {1980},
  journaltitle = {Cahiers de Topologie et G\'{e}om\'{e}trie Diff\'{e}rentielle},
  note = {Third Colloquium on Categories (Amiens, 1980), Part I},
  number = {4},
  pages = {377--392},
  volume = {21},
}

@misc{lawvere:laws-of-motion,
  title = {Toposes of laws of motion},
  author = {Lawvere, F. William},
  url = {https://github.com/mattearnshaw/lawvere/raw/master/pdfs/1997-toposes-of-laws-of-motion.pdf},
  date = {1997-09},
  note = {Talk transcript.},
}

@misc{lawvere:outline-sdg,
  title = {Outline of Synthetic Differential Geometry},
  author = {Lawvere, F. William},
  url = {https://github.com/mattearnshaw/lawvere/raw/master/pdfs/1998-outline-of-synthetic-differential-geometry.pdf},
  date = {1998-02},
  note = {Lecture notes.},
}

@incollection{lawvere:microphysics,
  title = {Categorical algebra for continuum micro physics},
  author = {Lawvere, F. William},
  date = {2002},
  doi = {10.1016/S0022-4049(02)00138-X},
  issn = {0022-4049},
  journaltitle = {J. Pure Appl. Algebra},
  note = {Special volume celebrating the 70th birthday of Professor Max Kelly},
  number = {1-3},
  pages = {267--287},
  volume = {175},
}

@article{lawvere:adjoints,
  title = {Left and right adjoint operations on spaces and data types},
  author = {Lawvere, F. William},
  date = {2004},
  doi = {10.1016/j.tcs.2004.01.026},
  issn = {0304-3975},
  journaltitle = tcs,
  number = {1-3},
  pages = {105--111},
  volume = {316},
}

@article{lawvere:adjointness-foundations,
  title = {Adjointness in foundations},
  author = {Lawvere, F. William},
  url = {http://www.tac.mta.ca/tac/reprints/articles/16/tr16abs.html},
  date = {2006},
  journaltitle = {Repr. Theory Appl. Categ.},
  note = {Reprinted from Dialectica {{\bf{2}}3} (1969)},
  number = {16},
  pages = {1--16},
}

@article{lawvere:cohesion,
  title = {Axiomatic Cohesion},
  author = {Lawvere, F. William},
  url = {http://www.tac.mta.ca/tac/volumes/19/3/19-03abs.html},
  date = {2007},
  journaltitle = tac,
  pages = {No. 3,41--49},
  volume = {19},
}

@incollection{lawvere:euler-vindicated,
  title = {Euler's continuum functorially vindicated},
  author = {Lawvere, F. William},
  booktitle = {Logic, mathematics, philosophy: vintage enthusiasms},
  date = {2011},
  doi = {10.1007/978-94-007-0214-1_13},
  pages = {249--254},
  publisher = {Springer, Dordrecht},
  series = {West. Ont. Ser. Philos. Sci.},
  volume = {75},
}

@inproceedings{lpvx:quipper-measurement,
  title = {Concrete Categorical Model of a Quantum Circuit Description Language with Measurement},
  author = {Lee, Dongho and Perrelle, Valentin and Valiron, Beno\^it and Xu, Zhaowei},
  booktitle = {41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  date = {2021},
  eprint = {2110.02691},
  eprintclass = {cs.LO},
  eprinttype = {arXiv},
  pubstate = {forthcoming},
  series = {FSTTCS '21},
}

@inproceedings{lee-park:magic-wand,
  title = {A proof system for separation logic with magic wand},
  author = {Lee, Wonyeol and Park, Sungwoo},
  booktitle = {Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  crossref = {popl:2014},
  doi = {10.1145/2535838.2535871},
  pages = {477--490},
}

@article{lumsdaine-shulman:hits,
  title = {Semantics of higher inductive types},
  author = {LeFanu Lumsdaine, Peter and Shulman, Michael},
  date = {2020},
  doi = {10.1017/s030500411900015x},
  issn = {0305-0041},
  journaltitle = {Mathematical Proceedings of the Cambridge Philosophical Society},
  number = {1},
  pages = {159--208},
  volume = {169},
}

@inproceedings{lops,
  title = {Internal Universes in Models of {Homotopy Type Theory}},
  author = {Licata, Daniel R. and Orton, Ian and Pitts, Andrew M. and Spitters, Bas},
  crossref = {fscd:2018},
  doi = {10.4230/LIPIcs.FSCD.2018.22},
  pages = {22:1--22:17},
}

@unpublished{lsr:depdep,
  title = {A Fibrational Framework for Substructural and Modal Dependent Type Theories},
  author = {Licata, Daniel R. and Riley, Mitchell and Shulman, Michael},
  date = {2022},
  pubstate = {inpreparation},
}

@inproceedings{ls:1var,
  title = {Adjoint Logic with a 2-Category of Modes},
  author = {Licata, Daniel R. and Shulman, Michael},
  url = {http://dlicata.web.wesleyan.edu/pubs/ls15adjoint/ls15adjoint.pdf},
  booktitle = {Logical foundations of computer science},
  date = {2016},
  doi = {10.1007/978-3-319-27683-0_16},
  pages = {219--235},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {9537},
}

@inproceedings{lsr:multi,
  title = {A Fibrational Framework for Substructural and Modal Logics},
  author = {Licata, Daniel R. and Shulman, Michael and Riley, Mitchell},
  url = {http://dlicata.web.wesleyan.edu/pubs/lsr17multi/lsr17multi-ex.pdf},
  crossref = {fscd:2017},
  doi = {10.4230/LIPIcs.FSCD.2017.25},
}

@inproceedings{rlz:focusing,
  title = {Focusing on Binding and Computation},
  author = {Licata, Daniel R. and Zeilberger, Noam and Harper, Robert},
  crossref = {lics:2008},
  doi = {10.1109/LICS.2008.48},
  pages = {241--252},
}

@inproceedings{eclnl,
  title = {Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams},
  author = {Lindenhovius, Bert and Mislove, Michael and Zamdzhiev, Vladimir},
  crossref = {lics:2018},
  doi = {10.1145/3209108.3209196},
}

@online{lumsdaine:frob-thread,
  title = {What is known and/or written about ``Frobenius eliminators''?},
  author = {Lumsdaine, Peter LeFanu},
  url = {https://groups.google.com/g/homotopytypetheory/c/b96TBt0Bn7Y/m/IiAcnUL2AQAJ},
  date = {2018-07},
}

@article{lumsdaine-warren:local-universes,
  title = {The Local Universes Model: An Overlooked Coherence Construction for Dependent Type Theories},
  author = {Lumsdaine, Peter LeFanu and Warren, Michael A.},
  date = {2015},
  doi = {10.1145/2754931},
  issn = {1529-3785},
  journaltitle = tocl,
  number = {3},
  pages = {Art. 23,31},
  volume = {16},
}

@online{lundfall:deplin,
  title = {A diagram model of linear dependent type theory},
  author = {Lundfall, Martin},
  date = {2018},
  eprint = {1806.09593},
  eprintclass = {math.LO},
  eprinttype = {arXiv},
}

@book{lurie:htt,
  title = {Higher topos theory},
  author = {Lurie, Jacob},
  date = {2009},
  doi = {10.1515/9781400830558},
  isbn = {978-0-691-14049-0},
  pages = {xviii+925},
  publisher = {Princeton University Press, Princeton, NJ},
  series = {Annals of Mathematics Studies},
  volume = {170},
}

@booklet{lurie:ha,
  title = {Higher Algebra},
  author = {Lurie, Jacob},
  url = {https://www.math.ias.edu/~lurie/papers/HA.pdf},
  date = {2017},
  publisher = {Harvard University},
}

@book{maclane-moerdijk:book,
  title = {Sheaves in geometry and logic},
  author = {Mac Lane, Saunders and Moerdijk, Ieke},
  date = {1994},
  isbn = {0-387-97710-4},
  pages = {xii+629},
  publisher = {Springer-Verlag, New York},
  series = {Universitext},
}

@article{marmolejo-menni:continuous-combinatorial,
  title = {On the relation between continuous and combinatorial},
  author = {Marmolejo, F. and Menni, M.},
  date = {2017},
  doi = {10.1007/s40062-016-0131-5},
  issn = {2193-8407},
  journaltitle = {J. Homotopy Relat. Struct.},
  number = {2},
  pages = {379--412},
  volume = {12},
}

@inproceedings{mvo:linearity-uniqueness,
  title = {Linearity and Uniqueness: An Entente Cordiale},
  author = {Marshall, Daniel and Vollmer, Michael and Orchard, Dominic},
  editor = {Sergey, Ilya},
  booktitle = {Programming Languages and Systems},
  date = {2022},
  doi = {10.1007/978-3-030-99336-8_13},
  isbn = {978-3-030-99336-8},
  location = {Cham},
  pages = {346--375},
  publisher = {Springer International Publishing},
}

@book{martin-lof:itt,
  title = {Intuitionistic Type Theory},
  author = {Martin-L\"{o}f, Per},
  url = {https://www.csie.ntu.edu.tw/~b94087/ITT.pdf},
  date = {1984},
  isbn = {88-7088-105-9},
  note = {Notes by Giovanni Sambin},
  pages = {iv+91},
  publisher = {Bibliopolis, Naples},
  series = {Studies in Proof Theory. Lecture Notes},
  volume = {1},
}

@article{may:wirthmuller-revisited,
  title = {The {W}irthm\"{u}ller isomorphism revisited},
  author = {May, J. P.},
  url = {http://www.tac.mta.ca/tac/volumes/11/5/11-05abs.html},
  date = {2003},
  journaltitle = tac,
  pages = {No. 5,132--142},
  volume = {11},
}

@book{may-sigurdsson,
  title = {Parametrized Homotopy Theory},
  author = {May, J. P. and Sigurdsson, J.},
  date = {2006},
  doi = {10.1090/surv/132},
  isbn = {978-0-8218-3922-5},
  pages = {x+441},
  publisher = {American Mathematical Society, Providence, RI},
  series = {Mathematical Surveys and Monographs},
  volume = {132},
}

@inbook{mcbride:nuttin,
  title = {I Got Plenty o' Nuttin'},
  author = {McBride, Conor},
  booktitle = {A list of successes that can change the world},
  date = {2016},
  doi = {10.1007/978-3-319-30936-1_12},
  pages = {207--233},
  publisher = {Springer International Publishing},
  series = {Lecture Notes in Computer Science},
  volume = {9600},
}

@article{menni:continuous-cohesion,
  title = {Continuous cohesion over sets},
  author = {Menni, M.},
  url = {http://www.tac.mta.ca/tac/volumes/29/20/29-20abs.html},
  date = {2014},
  journaltitle = {Theory Appl. Categ.},
  pages = {No. 20,542--568},
  volume = {29},
}

@article{menni:n-quantifiers,
  title = {About {$\text{\font\cyrss=wncyss10\cyrss I}$}-quantifiers},
  author = {Menni, Mat\'ias},
  date = {2003},
  doi = {10.1023/A:1025750816098},
  issn = {0927-2852},
  journaltitle = {Appl. Categ. Structures},
  number = {5},
  pages = {421--445},
  volume = {11},
}

@book{moerdijk-reyes:book,
  title = {Models for smooth infinitesimal analysis},
  author = {Moerdijk, Ieke and Reyes, Gonzalo E.},
  date = {1991},
  doi = {10.1007/978-1-4757-4143-8},
  isbn = {0-387-97489-X},
  pages = {x+399},
  publisher = {Springer-Verlag, New York},
}

@inproceedings{grtt,
  title = {Graded Modal Dependent Type Theory},
  author = {Moon, Benjamin and Eades III, Harley and Orchard, Dominic},
  editor = {Yoshida, Nobuko},
  booktitle = {Programming Languages and Systems},
  date = {2021},
  doi = {10.1007/978-3-030-72019-3_17},
  location = {Cham},
  pages = {462--490},
  publisher = {Springer International Publishing},
}

@inproceedings{mortberg-pujet:cube-synth,
  title = {Cubical Synthetic Homotopy Theory},
  author = {M\"{o}rtberg, Anders and Pujet, Lo\"ic},
  booktitle = {Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs},
  date = {2020},
  doi = {10.1145/3372885.3373825},
  isbn = {978-1-4503-7097-4},
  location = {New Orleans, LA, USA},
  pages = {158--171},
  publisher = acm,
  series = {CPP 2020},
}

@misc{jaz:modal-fracture,
  title = {Modal Fracture of Higher Groups},
  author = {Myers, David Jaz},
  date = {2021},
  eprint = {2106.15390},
  eprintclass = {math.CT},
  eprinttype = {arXiv},
  pubstate = {submitted},
}

@article{jaz:good-fibrations,
  title = {Good fibrations through the modal prism},
  author = {Myers, David Jaz},
  date = {2022},
  doi = {10.21136/HS.2022.04},
  journaltitle = {Higher Structures},
  number = {1},
  pages = {212--255},
  volume = {6},
}

@online{jaz:orbifolds,
  title = {Orbifolds as microlinear types in synthetic differential cohesive homotopy type theory},
  author = {Myers, David Jaz},
  date = {2022},
  eprint = {2205.15887},
  eprintclass = {math.AT},
  eprinttype = {arXiv},
}

@phdthesis{jaz:thesis,
  title = {Symmetry, Geometry, Modality},
  author = {Myers, David Jaz},
  url = {http://jhir.library.jhu.edu/handle/1774.2/67618},
  date = {2022},
  institution = {Johns Hopkins University},
}

@misc{jaz:microlinear,
  title = {Orbifolds as microlinear types in synthetic differential cohesive homotopy type theory},
  author = {Myers, David Jaz},
  date = {2022},
  eprint = {2205.15887},
  eprintclass = {math.AT},
  eprinttype = {arXiv},
}

@unpublished{jaz:toposes-lpc,
  title = {Toposes as Lex-Presentable Categories},
  author = {Myers, David Jaz},
  url = {http://xabier.garcia.martinez.webs.uvigo.gal/CT2024/files/Slides/Myers_Slides.pdf},
  date = {2024-06},
  location = {Santiago de Compostela, Spain},
  note = {Talk slides.},
  series = {CT2024},
}

@article{contextual-modal,
  title = {Contextual modal type theory},
  author = {Nanevski, Aleksandar and Pfenning, Frank and Pientka, Brigitte},
  date = {2008},
  doi = {10.1145/1352582.1352591},
  issn = {1529-3785},
  journaltitle = tocl,
  number = {3},
  pages = {Art. 23,49},
  volume = {9},
}

@article{ng-vickers:exponentiation,
  title = {Point-free construction of real exponentiation},
  author = {Ng, Ming and Vickers, Steven},
  date = {2022},
  doi = {10.46298/lmcs-18(3:15)2022},
  journaltitle = {Log. Methods Comput. Sci.},
  number = {3},
  pages = {Paper No. 15,32},
  volume = {18},
}

@misc{ng-vickers:ostrowski,
  title = {A Point-Free Look at Ostrowski's Theorem and Absolute Values},
  author = {Ng, Ming and Vickers, Steven},
  date = {2023},
  eprint = {2308.14758},
  eprintclass = {math.NT},
  eprinttype = {arXiv},
}

@online{nlab:synth-list,
  title = {Mathematics Presented in {Homotopy Type Theory}},
  author = {{nLab authors}},
  url = {https://ncatlab.org/nlab/show/mathematics+presented+in+homotopy+type+theory},
  date = {2019},
  shorthand = {nLab},
}

@online{nlab:dltt,
  title = {Dependent linear type theory},
  author = {{nLab authors}},
  url = {https://ncatlab.org/nlab/show/dependent+linear+type+theory},
  date = {2020},
  shorthand = {nLab},
}

@online{nlab:type-theoretic_model_category,
  title = {Type-theoretic model category},
  author = {{nLab authors}},
  url = {http://ncatlab.org/nlab/show/type-theoretic+model+category},
  date = {2020-01},
  shorthand = {nLab},
}

@inproceedings{nd:degrees-of-relatedness,
  title = {Degrees of Relatedness: A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory},
  author = {Nuyts, Andreas and Devriese, Dominique},
  booktitle = {Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science},
  date = {2018},
  doi = {10.1145/3209108.3209119},
  isbn = {978-1-4503-5583-4},
  keywords = {cubical type theory,presheaf semantics,Parametricity,erasure,unions,algebra in type theory,intersections,irrelevance},
  location = {Oxford, United Kingdom},
  pages = {779--788},
  publisher = acm,
  series = {LICS '18},
}

@article{transpension,
  title = {Transpension: The Right Adjoint to the Pi-type},
  author = {Nuyts, Andreas and Devriese, Dominique},
  date = {2021},
  eprint = {2008.08533v3},
  eprintclass = {cs.LO},
  eprinttype = {arXiv},
  journaltitle = lmcs,
  pubstate = {submitted},
}

@article{dependable-atomicity,
  title = {Dependable Atomicity in Type Theory},
  author = {Nuyts, Andreas and Devriese, Dominique},
  url = {https://lirias.kuleuven.be/retrieve/540872},
  crossref = {types:2019},
}

@article{nvd:parametric-quantifiers,
  title = {Parametric Quantifiers for Dependent Type Theory},
  author = {Nuyts, Andreas and Vezzosi, Andrea and Devriese, Dominique},
  date = {2017-08},
  doi = {10.1145/3110276},
  journaltitle = {Proc. ACM Program. Lang.},
  keywords = {Parametricity,cubical type theory,Agda,presheaf semantics,sized types},
  location = {New York, NY, USA},
  number = {ICFP},
  publisher = acm,
  volume = {1},
}

@article{ohearn:bunched-typing,
  title = {On bunched typing},
  author = {O'Hearn, Peter},
  date = {2003},
  doi = {10.1017/S0956796802004495},
  issn = {0956-7968},
  journaltitle = jfp,
  number = {4},
  pages = {747--796},
  volume = {13},
}

@article{op:bi,
  title = {The Logic of Bunched Implications},
  author = {O'Hearn, Peter W. and Pym, David J.},
  date = {1999},
  doi = {10.2307/421090},
  issn = {1079-8986},
  journaltitle = {Bulletin of Symbolic Logic},
  number = {2},
  pages = {215--244},
  volume = {5},
}

@article{granule,
  title = {Quantitative Program Reasoning with Graded Modal Types},
  author = {Orchard, Dominic and Liepelt, Vilem-Benjamin and Eades III, Harley},
  crossref = {icfp:2019},
  doi = {10.1145/3341714},
}

@article{orton-pitts:cubical,
  title = {Axioms for modelling cubical type theory in a topos},
  author = {Orton, Ian and Pitts, Andrew M.},
  date = {2018},
  doi = {10.23638/LMCS-14(4:23)2018},
  journaltitle = {Log. Methods Comput. Sci.},
  number = {4},
  pages = {Paper No. 23,33},
  volume = {14},
}

@inproceedings{orton-pitts:decomposing-univalence,
  title = {{Decomposing the Univalence Axiom}},
  author = {Orton, Ian and Pitts, Andrew M.},
  crossref = {types:2017},
  doi = {10.4230/LIPIcs.TYPES.2017.6},
  pages = {Art. No. 6,19},
}

@phdthesis{orton:2019,
  title = {Cubical Models of Homotopy Type Theory - An Internal Approach},
  author = {Orton, Richard Ian},
  date = {2019},
  doi = {10.17863/CAM.36690},
  institution = {University of Cambridge},
}

@inproceedings{depaiva-ritter:fibrational,
  title = {Fibrational Modal Type Theory},
  author = {de Paiva, Valeria and Ritter, Eike},
  booktitle = {Proceedings of the {T}enth {W}orkshop on {L}ogical and {S}emantic {F}rameworks, with {A}pplications ({LSFA} 2015)},
  date = {2016},
  doi = {10.1016/j.entcs.2016.06.010},
  pages = {143--161},
  series = entcs,
  volume = {323},
}

@inproceedings{qtt-style-coeffects,
  title = {Coeffects: A Calculus of Context-Dependent Computation},
  author = {Petricek, Tomas and Orchard, Dominic and Mycroft, Alan},
  crossref = {icfp:2014},
  doi = {10.1145/2628136.2628160},
}

@inproceedings{pfenning:intensionality,
  title = {Intensionality, extensionality, and proof irrelevance in modal type theory},
  author = {Pfenning, F.},
  booktitle = {Proceedings 16th Annual IEEE Symposium on Logic in Computer Science},
  date = {2001},
  doi = {10.1109/LICS.2001.932499},
  pages = {221--230},
}

@article{pfenning-davies,
  title = {A judgmental reconstruction of modal logic},
  author = {Pfenning, Frank and Davies, Rowan},
  date = {2001},
  doi = {10.1017/S0960129501003322},
  issn = {0960-1295},
  journaltitle = mscs,
  pages = {511--540},
  volume = {11},
}

@incollection{phoa:effective-domains,
  title = {Effective domains and intrinsic structure},
  author = {Phoa, Wesley},
  booktitle = {Fifth {A}nnual {IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({P}hiladelphia, {PA}, 1990)},
  date = {1990},
  doi = {10.1109/LICS.1990.113762},
  pages = {366--377},
  publisher = {IEEE Comput. Soc. Press, Los Alamitos, CA},
}

@article{pitts:alpha-recursion,
  title = {Structural recursion with locally scoped names},
  author = {Pitts, Andrew M.},
  date = {2011},
  doi = {10.1017/S0956796811000116},
  issn = {0956-7968},
  journaltitle = {J. Funct. Programming},
  number = {3},
  pages = {235--286},
  volume = {21},
}

@inproceedings{pmd:dttan,
  title = {A Dependent Type Theory with Abstractable Names},
  author = {Pitts, Andrew M. and Matthiesen, Justus and Derikx, Jasper},
  booktitle = {Ninth {W}orkshop on {L}ogical and {S}emantic {F}rameworks, with {A}pplications ({LSFA} 2014)},
  date = {2015},
  doi = {10.1016/j.entcs.2015.04.003},
  pages = {19--50},
  publisher = {Elsevier Sci. B. V., Amsterdam},
  series = entcs,
  volume = {312},
}

@article{ps:duality-and-traces,
  title = {Duality and traces for indexed monoidal categories},
  author = {Ponto, Kate and Shulman, Michael},
  url = {http://www.tac.mta.ca/tac/volumes/26/23/26-23abs.html},
  date = {2012},
  journaltitle = {Theory Appl. Categ.},
  pages = {No. 23,582--659},
  volume = {26},
}

@article{mike-kate:traces,
  title = {Traces in symmetric monoidal categories},
  author = {Ponto, Kate and Shulman, Michael},
  date = {2014},
  doi = {10.1016/j.exmath.2013.12.003},
  issn = {0723-0869},
  journaltitle = {Expositiones Mathematicae},
  number = {3},
  pages = {248--273},
  volume = {32},
}

@incollection{power-tanaka:binding-signatures,
  title = {Binding signatures for generic contexts},
  author = {Power, John and Tanaka, Miki},
  booktitle = {Typed lambda calculi and applications},
  date = {2005},
  doi = {10.1007/11417170_23},
  pages = {308--323},
  publisher = {Springer, Berlin},
  series = {Lecture Notes in Comput. Sci.},
  volume = {3461},
}

@book{pym:book,
  title = {The Semantics and Proof Theory of the Logic of Bunched Implications},
  author = {Pym, D. J.},
  date = {2002},
  doi = {10.1007/978-94-017-0091-7},
  publisher = {Kluwer Academic Publishers},
  related = {pym:book-erratum},
  relatedstring = {Errata in},
  series = {Applied Logic Series},
  volume = {26},
}

@online{pym:book-erratum,
  title = {Errata and Remarks for The Semantics and Proof Theory of the Logic of Bunched Implications},
  author = {Pym, D. J.},
  url = {http://www0.cs.ucl.ac.uk/staff/D.Pym/BI-monograph-errata.pdf},
  date = {2008},
}

@article{rasekh-stonek:cotangent,
  title = {The cotangent complex and {T}hom spectra},
  author = {Rasekh, Nima and Stonek, Bruno},
  date = {2020},
  doi = {10.1007/s12188-020-00226-8},
  issn = {0025-5858,1865-8784},
  journaltitle = {Abh. Math. Semin. Univ. Hambg.},
  number = {2},
  pages = {229--252},
  volume = {90},
}

@unpublished{reed:modal,
  title = {A Judgmental Deconstruction of Modal Logic},
  author = {Reed, Jason},
  url = {http://www.cs.cmu.edu/~jcreed/papers/jdml.pdf},
  date = {2009},
}

@phdthesis{reed:thesis,
  title = {A Hybrid Logical Framework},
  author = {Reed, Jason},
  url = {http://jcreed.org/papers/thesis-final-color.pdf},
  date = {2009},
  institution = {Carnegie Mellon University},
}

@unpublished{reed-pfenning:resource-semantics,
  title = {A Constructive Approach to the Resource Semantics of Substructural Logics},
  author = {Reed, Jason and Pfenning, Frank},
  url = {http://www.cs.cmu.edu/~jcreed/papers/rp-substruct.pdf},
  date = {2009},
}

@online{rezk:global-cohesion,
  title = {Global homotopy theory and cohesion},
  author = {Rezk, Charles},
  url = {https://faculty.math.illinois.edu/~rezk/global-cohesion.pdf},
  date = {2014},
}

@article{rs:synthetic-cats,
  title = {A type theory for synthetic {$\infty$}-categories},
  author = {Riehl, Emily and Shulman, Michael},
  date = {2017},
  doi = {10.1007/s42001-017-0005-6},
  journaltitle = {High. Struct.},
  number = {1},
  pages = {147--224},
  volume = {1},
}

@online{egbert:join,
  title = {The join construction},
  author = {Rijke, Egbert},
  date = {2017},
  eprint = {1701.07538},
  eprintclass = {math.CT},
  eprinttype = {arXiv},
}

@phdthesis{egbert:thesis,
  title = {Classifying Types},
  author = {Rijke, Egbert},
  date = {2018-07},
  eprint = {1906.09435},
  eprintclass = {math.LO},
  eprinttype = {arXiv},
  institution = {Carnegie Mellon University},
}

@article{rss:modalities,
  title = {Modalities in {Homotopy Type Theory}},
  author = {Rijke, Egbert and Shulman, Michael and Spitters, Bas},
  date = {2020},
  journaltitle = lmcs,
  number = {1},
  pages = {Paper No. 2,79},
  volume = {16},
}

@phdthesis{riley:thesis,
  title = {A Dependent Bunched Type Theory for Synthetic Stable Homotopy Theory},
  author = {Riley, Mitchell},
  date = {2022},
  doi = {10.14418/wes01.3.139},
  institution = {Wesleyan University},
}

@online{riley:tiny,
  title = {A Type Theory with a Tiny Object},
  author = {Riley, Mitchell},
  date = {2024},
  eprint = {2403.01939},
  eprintclass = {math.CT},
  eprinttype = {arXiv},
}

@online{rfl:spec-note,
  title = {Synthetic Spectra via a Monadic and Comonadic Modality},
  author = {Riley, Mitchell and Finster, Eric and Licata, Daniel R.},
  date = {2021},
  eprint = {2102.04099},
  eprintclass = {math.CT},
  eprinttype = {arXiv},
}

@unpublished{rl:lindep,
  title = {A Dependent Bunched Type Theory for Synthetic Stable Homotopy Theory},
  author = {Riley, Mitchell and Licata, Daniel R.},
  date = {2021},
  pubstate = {inpreparation},
}

@online{sati-schreiber:proper-orbifold-cohomology,
  title = {Proper Orbifold Cohomology},
  author = {Sati, Hisham and Schreiber, Urs},
  url = {https://ncatlab.org/schreiber/files/orbi220627.pdf},
  date = {2022-06},
}

@phdthesis{schopp:thesis,
  title = {Names and Binding in Type Theory},
  author = {Sch\"{o}pp, Ulrich},
  url = {https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.561934},
  date = {2006},
  institution = {University of Edinburgh},
}

@inproceedings{ss:dep-bunch,
  title = {A Dependent Type Theory with Names and Binding},
  author = {Sch\"{o}pp, Ulrich and Stark, Ian},
  booktitle = {Computer Science Logic},
  date = {2004},
  doi = {10.1007/978-3-540-30124-0_20},
  pages = {235--249},
  publisher = {Springer, Berlin},
  series = {Lecture Notes in Computer Science},
  volume = {3210},
}

@online{urs:lin,
  title = {Quantization via Linear homotopy types},
  author = {Schreiber, Urs},
  date = {2014},
  eprint = {1402.7041},
  eprintclass = {math-ph},
  eprinttype = {arXiv},
}

@online{urs:diff-coh,
  title = {Differential cohomology in a cohesive infinity-topos},
  author = {Schreiber, Urs},
  url = {https://ncatlab.org/schreiber/files/dcct170811.pdf},
  date = {2017},
}

@inproceedings{schreiber-shulman:cohesive,
  title = {Quantum Gauge Field Theory in Cohesive Homotopy Type Theory},
  author = {Schreiber, Urs and Shulman, Michael},
  booktitle = {Workshop on Quantum Physics and Logic},
  date = {2012},
  doi = {10.4204/EPTCS.158.8},
}

@article{mike:framed-bicategories,
  title = {Framed bicategories and monoidal fibrations},
  author = {Shulman, Michael},
  url = {http://www.tac.mta.ca/tac/volumes/20/18/20-18abs.html},
  date = {2008},
  journaltitle = tac,
  pages = {No. 18,650--738},
  volume = {20},
}

@article{mike:enriched-indexed,
  title = {Enriched indexed categories},
  author = {Shulman, Michael},
  url = {http://www.tac.mta.ca/tac/volumes/28/21/28-21abs.html},
  date = {2013},
  journaltitle = tac,
  pages = {616--696},
  volume = {28},
}

@article{mike:elegant-reedy,
  title = {The univalence axiom for elegant {Reedy} presheaves},
  author = {Shulman, Michael},
  date = {2015},
  doi = {10.4310/HHA.2015.v17.n2.a6},
  issn = {1532-0073},
  journaltitle = {Homology, Homotopy and Applications},
  number = {2},
  pages = {81--106},
  volume = {17},
}

@online{mike:catlog,
  title = {Categorical logic from a categorical point of view},
  author = {Shulman, Michael},
  url = {https://mikeshulman.github.io/catlog/catlog.pdf},
  date = {2016},
}

@article{mike:real-cohesive-hott,
  title = {Brouwer's fixed-point theorem in real-cohesive homotopy type theory},
  author = {Shulman, Michael},
  date = {2018},
  doi = {10.1017/S0960129517000147},
  issn = {0960-1295},
  journaltitle = mscs,
  number = {6},
  pages = {856--941},
  volume = {28},
}

@online{mike:all,
  title = {All $(\infty, 1)$-toposes have strict univalent universes},
  author = {Shulman, Michael},
  date = {2019},
  eprint = {1904.07004},
  eprintclass = {math.AT},
  eprinttype = {arXiv},
}

@online{hott:blakers-massey-formalised,
  title = {The Generalized Blakers-Massey Theorem},
  author = {Shulman, Michael},
  url = {https://github.com/HoTT/HoTT/blob/master/theories/Homotopy/BlakersMassey.v},
  date = {2019},
  organization = {The HoTT Library},
}

@article{shulman:practical-smc,
  title = {A practical type theory for symmetric monoidal categories},
  author = {Shulman, Michael},
  url = {http://www.tac.mta.ca/tac/volumes/37/25/37-25abs.html},
  date = {2021},
  journaltitle = tac,
  pages = {863--907},
  volume = {37},
}

@unpublished{mike:observational-day3,
  title = {Higher Observational Type Theory},
  author = {Shulman, Michael and Altenkirch, Thorsten and Kaposi, Ambrus},
  url = {https://home.sandiego.edu/~shulman/papers/hott-cmu-day3.pdf},
  date = {2022},
  note = {Talk slides.},
}

@online{lean:spectra,
  title = {Spectral Sequences in {Homotopy Type Theory}},
  author = {Shulman, Michael and van Doorn, Floris and Rijke, Egbert and Piceghello, Stefano and Sulyma, Yuri},
  url = {https://github.com/cmu-phil/Spectral/tree/master/spectrum},
  date = {2019},
}

@inproceedings{sbr:seq-colims,
  title = {Sequential Colimits in {Homotopy Type Theory}},
  author = {Sojakova, Kristina and van Doorn, Floris and Rijke, Egbert},
  crossref = {lics:2020},
  doi = {10.1145/3373718.3394801},
}

@phdthesis{sterling:thesis,
  title = {First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory},
  author = {Sterling, Jonathan},
  date = {2021},
  doi = {10.5281/zenodo.14210117},
  institution = {Carnegie Mellon University},
}

@book{streicher:book,
  title = {Semantics of Type Theory},
  author = {Streicher, Thomas},
  date = {1991},
  doi = {10.1007/978-1-4612-0433-6},
  isbn = {0-8176-3594-7},
  pages = {xii+298},
  publisher = {Birkh\"{a}user Boston, Inc., Boston, MA},
  series = {Progress in Theoretical Computer Science},
}

@misc{swan:oracle-modalities,
  title = {Oracle modalities},
  author = {Swan, Andrew W},
  date = {2024},
  eprint = {2406.05818},
  eprintclass = {math.LO},
  eprinttype = {arXiv},
}

@article{tsementzis:morita,
  title = {A syntactic characterization of {M}orita equivalence},
  author = {Tsementzis, Dimitris},
  date = {2017},
  doi = {10.1017/jsl.2017.59},
  issn = {0022-4812},
  journaltitle = {J. Symb. Log.},
  number = {4},
  pages = {1181--1198},
  volume = {82},
}

@incollection{uemura:cubical-assemblies,
  title = {Cubical assemblies, a univalent and impredicative universe and a failure of propositional resizing},
  author = {Uemura, Taichi},
  booktitle = {24th {I}nternational {C}onference on {T}ypes for {P}roofs and {P}rograms},
  date = {2019},
  doi = {10.4230/LIPIcs.TYPES.2018.7},
  pages = {Art. No. 7,20},
  publisher = {Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern},
  series = {LIPIcs. Leibniz Int. Proc. Inform.},
  volume = {130},
}

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

@inproceedings{vakar:lin-lf,
  title = {A Categorical Semantics for Linear Logical Frameworks},
  author = {V\'{a}k\'{a}r, Matthijs},
  crossref = {fossacs:2015},
  doi = {10.1007/978-3-662-46678-0_7},
  pages = {102--116},
}

@online{vakar:deplin,
  title = {Syntax and Semantics of Linear Dependent Types},
  author = {V\'{a}k\'{a}r, Matthjis},
  date = {2014},
  eprint = {1405.0033},
  eprintclass = {cs.AT},
  eprinttype = {arXiv},
}

@phdthesis{floris:thesis,
  title = {On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory},
  author = {{van Doorn}, Floris},
  date = {2018},
  eprint = {1808.10690},
  eprintclass = {math.AT},
  eprinttype = {arXiv},
}

@online{agda-flat,
  title = {Agda Flat},
  author = {Vezzosi, Andrea},
  url = {https://github.com/agda/agda/tree/flat},
  date = {2019},
}

@article{vickers:cats-domains,
  title = {Topical categories of domains},
  author = {Vickers, Steven},
  date = {1999},
  doi = {10.1017/S0960129599002741},
  issn = {0960-1295},
  journaltitle = {Math. Structures Comput. Sci.},
  number = {5},
  pages = {569--616},
  volume = {9},
}

@article{vickers:continuity,
  title = {Continuity and geometric logic},
  author = {Vickers, Steven},
  date = {2014},
  doi = {10.1016/j.jal.2013.07.004},
  issn = {1570-8683},
  journaltitle = {J. Appl. Log.},
  number = {1},
  pages = {14--27},
  volume = {12},
}

@misc{vickers:point-free,
  title = {Generalized point-free spaces, pointwise},
  author = {Vickers, Steven},
  date = {2022},
  eprint = {2206.01113},
  eprintclass = {math.CT},
  eprinttype = {arXiv},
}

@techreport{clf,
  title = {A concurrent logical framework I: Judgments and properties},
  author = {Watkins, Kevin and Cervesato, Iliano and Pfenning, Frank and Walker, David},
  url = {https://www.cs.cmu.edu/~fp/papers/CMU-CS-02-101.pdf},
  date = {2003},
  institution = {Carnegie Mellon University},
  number = {CMU-CS-02-101},
}

@inproceedings{wood-atkey:lin-algebra-metatheory,
  title = {A Linear Algebra Approach to Linear Metatheory},
  author = {Wood, James and Atkey, Robert},
  booktitle = {Linearity/TLLA '20},
  date = {2020},
  eprint = {2005.02247},
  eprintclass = {cs.PL},
  eprinttype = {arXiv},
}

@article{wraith:generic-interval,
  title = {Using the generic interval},
  author = {Wraith, Gavin C.},
  url = {http://www.numdam.org/item/CTGDC_1993__34_4_259_0/},
  date = {1993},
  journaltitle = {Cahiers de Topologie et G\'{e}om\'{e}trie Diff\'{e}rentielle Cat\'{e}goriques},
  number = {4},
  pages = {259--266},
  volume = {34},
}

@article{yetter:tiny,
  title = {On right adjoints to exponential functors},
  author = {Yetter, David},
  date = {1987},
  doi = {10.1016/0022-4049(87)90077-6},
  issn = {0022-4049},
  journaltitle = {Journal of Pure and Applied Algebra},
  number = {3},
  pages = {287--304},
  related = {yetter:tiny-erratum},
  relatedstring = {See also},
  volume = {45},
}

@article{yetter:tiny-erratum,
  title = {Corrections to: ``{O}n right adjoints to exponential functors''},
  author = {Yetter, David},
  date = {1989},
  doi = {10.1016/0022-4049(89)90056-X},
  issn = {0022-4049},
  journaltitle = {Journal of Pure and Applied Algebra},
  number = {1},
  pages = {103--105},
  volume = {58},
}

@unpublished{zeilberger:modal-bi,
  title = {Modal BI and Separation Logic},
  author = {Zeilberger, Noam},
  url = {http://www.cs.cmu.edu/~noam/papers/s4bi.pdf},
  date = {2005},
}

@phdthesis{zeilberger:thesis,
  title = {The Logical Basis of Evaluation Order and Pattern-Matching},
  author = {Zeilberger, Noam},
  url = {https://www.cs.cmu.edu/~rwh/theses/zeilberger.pdf},
  date = {2009},
  institution = {Carnegie Mellon University},
}

@inproceedings{zwanziger:comonadic,
  title = {Natural Model Semantics for Comonadic and Adjoint Type Theory: Extended Abstract},
  author = {Zwanziger, Colin},
  url = {http://www.cs.ox.ac.uk/ACT2019/preproceedings/Colin%20Zwanziger%20Natural%20Model%20Semantics%20for%20Comonadic%20and%20Adjoint%20Modal%20Type%20Theory.pdf},
  booktitle = {Preproceedings of the Applied Category Theory Conference 2019},
  date = {2019},
}