Initial Overleaf Import

Author: ionathanch

biblio.bib

@@ -0,0 +1,290 @@
+@inbook{synsem,
+    place={Cambridge},
+    series={Publications of the Newton Institute},
+    title={{Syntax and Semantics of Dependent Types}},
+    DOI={10.1017/CBO9780511526619.004},
+    booktitle={Semantics and Logics of Computation},
+    publisher={Cambridge University Press},
+    author={Hofmann, Martin},
+    year={1997},
+    pages={79-–130}, 
+    collection={Publications of the Newton Institute}
+}
+
+@inproceedings{exteq,
+    author={Altenkirch, Thorsten},
+    booktitle={Proceedings of the 14th Symposium on Logic in Computer Science}, 
+    title={{Extensional equality in intensional type theory}},
+    year={1999},
+    pages={412--420},
+    doi={10.1109/LICS.1999.782636}
+}
+
+@inproceedings{relparam,
+    author = {Atkey, Robert and Ghani, Neil and Johann, Patricia},
+    title = {{A Relationally Parametric Model of Dependent Type Theory}},
+    year = {2014},
+    isbn = {9781450325448},
+    publisher = {Association for Computing Machinery},
+    address = {New York, NY, USA},
+    doi = {10.1145/2535838.2535852},
+    booktitle = {Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
+    pages = {503-515},
+    numpages = {13},
+    location = {San Diego, California, USA},
+    series = {POPL '14}
+}
+
+@article{mdtt,
+    title={{Modal dependent type theory and dependent right adjoints}},
+    volume={30},
+    DOI={10.1017/S0960129519000197},
+    number={2},
+    journal={Mathematical Structures in Computer Science},
+    publisher={Cambridge University Press},
+    author={Birkedal, Lars and Clouston, Ranald and Mannaa, Bassel and Ejlers Møgelberg, Rasmus and Pitts, Andrew M. and Spitters, Bas},
+    year={2020},
+    pages={118–138}
+}
+
+@article{abstractable,
+    title = {{A Dependent Type Theory with Abstractable Names}},
+    journal = {Electronic Notes in Theoretical Computer Science},
+    volume = {312},
+    pages = {19--50},
+    year = {2015},
+    note = {Ninth Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2014)},
+    issn = {1571-0661},
+    doi = {10.1016/j.entcs.2015.04.003},
+    url = {https://www.sciencedirect.com/science/article/pii/S1571066115000079},
+    author = {Andrew M. Pitts and Justus Matthiesen and Jasper Derikx}
+}
+
+@inproceedings{contextual,
+    author = {Pientka, Brigitte and Sch\"{o}pp, Ulrich},
+    title = {{Semantical Analysis of Contextual Types}},
+    year = {2020},
+    isbn = {978-3-030-45230-8},
+    publisher = {Springer-Verlag},
+    address = {Berlin, Heidelberg},
+    doi = {10.1007/978-3-030-45231-5\_26},
+    booktitle = {Foundations of Software Science and Computation Structures: 23rd International Conference},
+    pages = {502–-521},
+    numpages = {20},
+    location = {Dublin, Ireland}
+}
+
+@article{undeceq,
+    TITLE = {{Undecidability of Equality in the Free Locally Cartesian Closed Category (Extended version)}},
+    AUTHOR = {Simon Castellan and Pierre Clairambault and Peter Dybjer},
+    DOI = {10.23638/LMCS-13(4:22)2017},
+    JOURNAL = {Logical Methods in Computer Science},
+    VOLUME = {13},
+    NUMBER = {4},
+    YEAR = {2017},
+    MONTH = Nov
+}
+
+@article{gatcwf,
+    title={{On generalized algebraic theories and categories with families}},
+    volume={31},
+    DOI={10.1017/S0960129521000268},
+    number={9},
+    journal={Mathematical Structures in Computer Science},
+    publisher={Cambridge University Press},
+    author={Bezem, Marc and Coquand, Thierry and Dybjer, Peter and Escard\'o, Mart\'in},
+    year={2021},
+    pages={1006-–1023}
+}
+
+@inproceedings{qtt,
+    author = {Atkey, Robert},
+    title = {{Syntax and Semantics of Quantitative Type Theory}},
+    year = {2018},
+    isbn = {9781450355834},
+    publisher = {Association for Computing Machinery},
+    address = {New York, NY, USA},
+    doi = {10.1145/3209108.3209189},
+    booktitle = {Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science},
+    pages = {56–-65},
+    numpages = {10},
+    location = {Oxford, United Kingdom},
+    series = {LICS '18}
+}
+
+@article{cwf,
+   title={{Categories with Families: Unityped, Simply Typed, and Dependently Typed}},
+   ISBN={9783030665456},
+   ISSN={2211-2766},
+   DOI={10.1007/978-3-030-66545-6_5},
+   journal={Outstanding Contributions to Logic},
+   publisher={Springer International Publishing},
+   author={Castellan, Simon and Clairambault, Pierre and Dybjer, Peter},
+   year={2021},
+   pages={135–-180}
+}
+
+@InProceedings{itt,
+  author={Dybjer, Peter},
+  editor={Berardi, Stefano and Coppo, Mario},
+  title={Internal type theory},
+  booktitle={Types for Proofs and Programs},
+  year={1996},
+  publisher={Springer Berlin Heidelberg},
+  address={Berlin, Heidelberg},
+  pages={120--134},
+  isbn={978-3-540-70722-6},
+  doi={10.1007/3-540-61780-9\_66}
+}
+
+@phdthesis{actt,
+  author = {Uemara, Taichi},
+  title = {Abstract and Concrete Type Theories},
+  school = {Institute for Logic, Language and Computation},
+  year = {2021},
+  month = {Jul},
+  doi = {11245.1/41ff0b60-64d4-4003-8182-c244a9afab3b},
+  url = {https://hdl.handle.net/11245.1/41ff0b60-64d4-4003-8182-c244a9afab3b}
+}
+
+@phdthesis{gat,
+  author = {Cartmell, John W.},
+  title = {Generalised algebraic theories and contextual categories},
+  school = {University of Oxford},
+  year = {1978}
+}
+
+@article{nat,
+  title={{Natural models of homotopy type theory}},
+  volume={28},
+  ISSN={1469-8072},
+  DOI={10.1017/s0960129516000268},
+  number={2},
+  journal={Mathematical Structures in Computer Science},
+  publisher={Cambridge University Press (CUP)},
+  author={Awodey, Steve},
+  year={2016},
+  month={Nov},
+  pages={241–-286}
+}
+
+@phdthesis{algnat,
+  author = {Newstead, Clive},
+  title = {Algebraic Models of Dependent Type Theory},
+  school = {Carnegie Mellon University},
+  year = 2018,
+  month = Aug,
+  doi = {10.1184/R1/7195124.v1},
+  url = {https://kilthub.cmu.edu/articles/thesis/Algebraic\_Models\_of\_Dependent\_Type\_Theory/7195124/1}
+}
+
+@InProceedings{shallow,
+    author={Kaposi, Ambrus and Kov{\'a}cs, Andr{\'a}s and Kraus, Nicolai},
+    editor={Hutton, Graham},
+    title={{Shallow Embedding of Type Theory is Morally Correct"}},
+    booktitle={Mathematics of Program Construction},
+    year=2019,
+    publisher={Springer International Publishing},
+    address={Cham},
+    pages={329--365},
+    isbn={978-3-030-33636-3},
+    doi={10.1007/978-3-030-33636-3\_12}
+}
+
+@InProceedings{hierarchy,
+  author =	{Kov\'{a}cs, Andr\'{a}s},
+  title =	{{Generalized Universe Hierarchies and First-Class Universe Levels}},
+  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
+  pages =	{28:1--28:17},
+  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
+  ISBN =	{978-3-95977-218-1},
+  ISSN =	{1868-8969},
+  year =	{2022},
+  volume =	{216},
+  editor =	{Manea, Florin and Simpson, Alex},
+  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
+  address =	{Dagstuhl, Germany},
+  URN =		{urn:nbn:de:0030-drops-157485},
+  doi =		{10.4230/LIPIcs.CSL.2022.28}
+}
+
+@inproceedings{kipling,
+  author = {McBride, Conor},
+  title = {{Outrageous but Meaningful Coincidences: Dependent Type-Safe Syntax and Evaluation}},
+  year = {2010},
+  isbn = {9781450302517},
+  publisher = {Association for Computing Machinery},
+  address = {New York, NY, USA},
+  doi = {10.1145/1863495.1863497},
+  booktitle = {Proceedings of the 6th ACM SIGPLAN Workshop on Generic Programming},
+  pages = {1–12},
+  numpages = {12},
+  location = {Baltimore, Maryland, USA},
+  series = {WGP '10}
+}
+
+@phdthesis{ext,
+  author = {Hofmann, Martin},
+  school = {University of Edinburgh},
+  title = {{Extensional concepts in intensional type theory}},
+  year = 1995,
+  month = Jul,
+  address = {Edinburgh, Scotland},
+  url = {http://www.lfcs.inf.ed.ac.uk/reports/95/ECS-LFCS-95-327/}
+}
+
+@article{obseq,
+  author = {Pujet, Lo\"{\i}c and Tabareau, Nicolas},
+  title = {{Observational Equality: Now for Good}},
+  year = {2022},
+  publisher = {Association for Computing Machinery},
+  address = {New York, NY, USA},
+  volume = {6},
+  number = {POPL},
+  doi = {10.1145/3498693},
+  journal = {Proceedings of the ACM on Programming Languages},
+  month = {jan},
+  articleno = {32},
+  numpages = {27},
+}
+
+@incollection{groupoid,
+    author = {Hofmann, Martin and Streicher, Thomas},
+    isbn = {9780198501275},
+    title = {{The groupoid interpretation of type theory}},
+    booktitle = {Twenty Five Years of Constructive Type Theory},
+    publisher = {Oxford University Press},
+    year = {1998},
+    month = {10},
+    doi = {10.1093/oso/9780198501275.003.0008},
+}
+
+@book{D-sets,
+	location = {Boston, {MA}},
+	title = {{Semantics of Type Theory}},
+	isbn = {978-1-4612-6757-7 978-1-4612-0433-6},
+	publisher = {Birkh\"auser Boston},
+	author = {Streicher, Thomas},
+	year = {1991},
+	doi = {10.1007/978-1-4612-0433-6},
+}
+
+@InProceedings{Lambda-sets,
+    author="Altenkirch, Thorsten",
+    editor="Barendregt, Henk and Nipkow, Tobias",
+    title={Proving strong normalization of CC by modifying realizability semantics},
+    booktitle="Types for Proofs and Programs",
+    year="1994",
+    publisher="Springer Berlin Heidelberg",
+    address="Berlin, Heidelberg",
+    pages="3--18",
+    isbn="978-3-540-48440-0",
+    doi="10.1007/3-540-58085-9\_70"
+}
+
+@unpublished{presheaf,
+    author = {Laouar, Alexis},
+    title = {{A presheaf model of dependent type theory}},
+    year = 2017,
+    url = {https://perso.crans.org/alaouar/rapportm1.pdf}
+}