biblio.bib

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