tiny.bib

@string{acm = "Association for Computing Machinery"}
@string{lmcs = "Logical Methods in Computer Science"}
@string{tac = "Theory and Applications of Categories"}

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

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

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

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

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

@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},
  editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
  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},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  volume = {152},
}

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

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

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

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

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

@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 = {Theoretical Computer Science},
  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},
}

@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},
  shorthand = {LOPS18},
}

@article{transpension,
  title = {Transpension: The Right Adjoint to the Pi-type},
  author = {Nuyts, Andreas and Devriese, Dominique},
  date = {2021},
  eprint = {2008.08533},
  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{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},
}