biblio.bib

% Journal articles and tech reports

@techreport{CoC,
  title = {{The calculus of constructions}},
  author = {Coquand, Thierry and Huet, G{\'e}rard},
  url = {https://hal.inria.fr/inria-00076024},
  number = {RR-0530},
  institution = {INRIA},
  year = 1986,
  month = May,
}

@techreport{GCC-Coquand,
  title = {{An analysis of Girard's paradox}},
  author = {Coquand, Thierry},
  url = {https://hal.inria.fr/inria-00076023},
  number = {RR-0531},
  institution = {INRIA},
  year = 1986,
  month = May,
}

@techreport{GCC-Luo,
  title = {{CC$^\infty_\subset$ and Its Meta Theory}},
  author = {Luo, Zhaohui},
  year = 1988,
  month = Jul,
  institution = {University of Edinburgh},
  url = {https://www.lfcs.inf.ed.ac.uk/reports/88/ECS-LFCS-88-58/}
}

@techreport{pCuIC,
  title = {{Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC)}},
  author = {Timany, Amin and Sozeau, Matthieu},
  url = {https://hal.inria.fr/hal-01615123},
  number = {RR-9105},
  institution = {KU Leuven, Belgium; Inria Paris},
  year = 2017,
  month = Oct,
}

@article{universes,
  title = {{Type checking with universes}},
  volume = {89},
  issn = {0304-3975},
  doi = {10.1016/0304-3975(90)90108-T},
  number = {1},
  journal = {Theoretical Computer Science},
  publisher = {Elsevier},
  author = {Harper, Robert and Pollack, Robert},
  month = Oct,
  year = 1991,
  pages = {107--136}
}

@article{Takahashi,
  title = {{Parallel reductions in $\lambda$-calculus}},
  journal = {Journal of Symbolic Computation},
  volume = {7},
  number = {2},
  pages = {113--123},
  year = 1989,
  month = Feb,
  issn = {0747-7171},
  doi = {10.1016/S0747-7171(89)80045-8},
  author = {Takahashi, Masako},
  publisher = {Elsevier}
}

@article{confluence,
  title = {{A Simplified Proof of the Church--Rosser Theorem}},
  author = {Komori, Yuichi and Matsuda, Naosuke and Yamakawa, Fumika},
  journal = {Studia Logica},
  volume = {102},
  number = {1},
  pages = {175--183},
  year = 2014,
  month = Feb,
  doi = {10.1007/s11225-013-9470-y},
  issn = {0039-3215},
  eissn = {1572-8730},
  publisher = {Institute of Philosophy and Sociology of the Polish Academy of Sciences},
}

@article{lambda-hat,
  title = {{Type-based termination of recursive definitions}},
  volume = {14},
  number = {1},
  issn = {0960-1295},
  eissn = {1469-8072},
  doi = {10.1017/S0960129503004122},
  journal = {Mathematical Structures in Computer Science},
  publisher = {Cambridge University Press},
  author = {Barthe, Gilles and Frade, Maria Jo\~ao and Gim\'enez, Eduardo and Pinto, Lu\'is and Uustalu, Tarmo},
  month = Feb,
  year = 2004,
  pages = {97--141},
}

@article{F-omega-cop,
  title = {{Well-founded recursion with copatterns and sized types}},
  volume = {26},
  number = {e2},
  doi = {10.1017/S0956796816000022},
  journal = {Journal of Functional Programming},
  publisher = {Cambridge University Press},
  author = {Abel, Andreas and Pientka, Brigitte},
  year = 2016,
  numpages = {61}
}

@article{CIC-unifier,
  title = {{A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading}},
  volume = {27},
  doi = {10.1017/S0956796817000028},
  journal = {Journal of Functional Programming},
  publisher = {Cambridge University Press},
  author = {Ziliani, Beta and Sozeau, Matthieu},
  year = 2017,
  number = {e10},
  numpages = {63},
  url = {https://hal.inria.fr/hal-01671925}
}

@article{unification,
  title = {{Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory}},
  volume = {28},
  number = {e12},
  doi = {10.1017/S095679681800014X},
  journal = {Journal of Functional Programming},
  publisher = {Cambridge University Press},
  author = {Cockx, Jesper and Devriese, Dominique},
  year = 2018,
  numpages = {55}
}

@article{telescope,
  title = {{Telescopic mappings in typed lambda calculus}},
  journal = {Information and Computation},
  volume = {91},
  number = {2},
  pages = {189--204},
  year = 1991,
  issn = {0890-5401},
  doi = {10.1016/0890-5401(91)90066-B},
  author = {{de Bruijn}, Nicolaas Govert},
  publisher = {Elsevier}
}

@article{accessibility,
  title = {{Terminating general recursion}},
  volume = {28},
  issn = {0006-3835},
  eissn = {1572-9125},
  doi = {10.1007/BF01941137},
  pages = {605--619},
  journal = {Tidskrift f\"or Informationsbehandling (BIT)},
  author = {Nordstr\"om, Bengt},
  year = 1988,
  publisher = {BIT foundation}
}

@article{pCIC,
  title = {{Proof-irrelevant model of CC with predicative induction and judgmental equality}},
  volume = {7},
  issn = {1860-5974},
  doi = {10.2168/LMCS-7(4:5)2011},
  pages = {5:1--5:25},
  number = {4},
  journal = {Logical Methods in Computer Science},
  author = {Lee, Gyesik and Werner, Benjamin},
  year = 2011,
  month = Nov
}

@article{impred-proof-irrel,
  title = {{Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality}},
  author = {Abel, Andreas and Coquand, Thierry},
  doi = {10.23638/LMCS-16(2:14)2020},
  journal = {Logical Methods in Computer Science},
  volume = {16},
  number = {2},
  year = 2020,
  pages = {14:1--14:5},
  month = Jun
}

@article{term-check,
  author = {Abel, Andreas},
  title = {{Termination Checking with Types}},
  journal = {RAIRO - Theoretical Informatics and Applications},
  year = 2004,
  doi = {10.1051/ita:2004015},
  volume = {38},
  number = {4},
  pages = {277--319},
  note = {Fixed Points in Computer Science (FICS '03)},
  publisher = {EDP Sciences}
}

@article{NbE,
  author = {Abel, Andreas and Vezzosi, Andrea and Winterhalter, Theo},
  title = {{Normalization by Evaluation for Sized Dependent Types}},
  year = 2017,
  month = Sep,
  publisher = {Association for Computing Machinery},
  volume = {1},
  number = {ICFP},
  doi = {10.1145/3110277},
  journal = {Proceedings of the ACM on Programming Languages},
  numpages = {30},
}

@article{conversion,
  author = {Abel, Andreas and \"{O}hman, Joakim and Vezzosi, Andrea},
  title = {{Decidability of Conversion for Type Theory in Type Theory}},
  year = 2017,
  month = Jan,
  publisher = {Association for Computing Machinery},
  volume = {2},
  number = {POPL},
  doi = {10.1145/3158111},
  journal = {Proceedings of the ACM on Programming Languages},
  month = Dec,
  numpages = {29}
}

@article{SProp,
  author = {Gilbert, Ga\"{e}tan and Cockx, Jesper and Sozeau, Matthieu and Tabareau, Nicolas},
  title = {{Definitional Proof-Irrelevance without K}},
  year = 2019,
  month = Jan,
  publisher = {Association for Computing Machinery},
  volume = {3},
  number = {POPL},
  doi = {10.1145/3290316},
  journal = {Proceedings of the ACM on Programming Languages},
  numpages = {28}
}

@article{phantom,
  author = {Van der Greer, J. and Hanraads, J. A. J. and Lupton, R. A.},
  year = 2000,
  title = {{The art of writing a scientific article}},
  journal = {Journal of Scientific Communications},
  volume = {163},
  number = {2},
  pages = {51--59}
}

% Dissertations, theses, and books

@phdthesis{lambda-hat-diss,
  title = {{Type-Based Termination of Recursive Definitions and Constructor Subtyping in Typed Lambda Calculi}},
  year = 2004,
  month = Mar,
  school = {University of Minho},
  address = {Braga, Portugal},
  url = {https://haslab.uminho.pt/sites/default/files/mjf/files/thesis.pdf},
  author = {Frade, Maria Jo{\~a}o}
}

@phdthesis{CIC-hat-minus,
  title = {{On type-based termination and dependent pattern matching in the calculus of inductive constructions}},
  author = {Sacchini, Jorge Luis},
  url = {https://pastel.archives-ouvertes.fr/pastel-00622429},
  school = {\'Ecole Nationale Sup\'erieure des Mines de Paris},
  address = {Paris, France},
  year = 2011,
  month = Jun
}

@phdthesis{Abel-diss,
  title = {{A Polymorphic Lambda-Calculus with Sized Higher-Order Types}},
  author = {Abel, Andreas},
  year = 2006,
  month = Jun,
  url = {http://www.cse.chalmers.se/~abela/diss.pdf},
  publisher = {Harland media},
  school = {Ludwig Maximilian University of Munich},
  address = {Munich, Germany}
}

@phdthesis{wjb,
  title = {{Compiling with Dependent Types}},
  author = {Bowman, William J.},
  address = {Boston, Massachussetts, USA},
  school = {Northeastern University},
  year = 2018,
  month = Nov,
  url = {http://hdl.handle.net/2047/D20316239},
  doi = {10.17760/D20316239}
}

@phdthesis{guarded,
  author = {Vezzosi, Andrea},
  school = {Chalmers University of Technology and University of Gothenburg},
  title = {{Guarded Recursive Types in Type Theory}},
  year = 2015,
  url = {https://research.chalmers.se/en/publication/226096},
  address = {G\"oteborg, Sweden},
  type = {Licentiate thesis}
}

@phdthesis{barras,
  author = {Barras, Bruno},
  school = {Universit\'e Paris-Diderot},
  title = {{Semantical Investigations in Intuitionistic Set Theory and Type Theories with Inductive Families}},
  year = 2012,
  type = {Habilitation thesis},
  url = {http://www.lsv.fr/~barras/habilitation/},
  address = {Paris, France},
}

@phdthesis{Agda,
  author = {Norell, Ulf},
  school = {Chalmers University of Technology and G\"oteborg University},
  title = {Towards a practical programming language based on dependent type theory},
  year = 2007,
  url = {https://research.chalmers.se/en/publication/46311},
  address = {G\"oteborg, Sweden}
}

@phdthesis{Arend,
  author = {Clifton, Andrew V.},
  school = {California State University},
  title = {{Arend --- Proof-assistant assisted pedagogy}},
  year = 2015,
  address = {Fresno, California, USA},
  url = {https://staffwww.fullcoll.edu/aclifton/files/arend-report.pdf},
  type = {Master's thesis}
}

@phdthesis{extensional-concepts,
  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/}
}

@book{MLTT,
  author = {Martin-L{\"o}f, Per},
  isbn = {88-7088-105-9},
  mrclass = {03B15 (03F50 03F55)},
  mrnumber = {769301 (86j:03005)},
  mrreviewer = {M. M. Richter},
  pages = {iv+91},
  publisher = {Bibliopolis},
  series = {Studies in Proof Theory},
  note = {Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980},
  title = {Intuitionistic type theory},
  volume = {1},
  year = 1984
}

% Conference proceedings

@inproceedings{F-hat,
  author = {Barthe, Gilles and Gr\'egoire, Benjamin and Pastawski, Fernando},
  title = {{Practical inference for type-based termination in a polymorphic setting}},
  booktitle = {Typed Lambda Calculi and Applications},
  series = {Lecture Notes in Computer Science},
  year = 2005,
  volume = {3461},
  pages = {71--85},
  publisher = {Springer-Verlag Berlin Heidelberg},
  affiliation = {Univ Nacl Cordoba, FaMAF, RA-5000 Cordoba, Argentina},
  doi = {10.1007/11417170\_7},
  issn = {0302-9743},
  isbn = {3-540-25593-1}
}

@inproceedings{CIC-hat,
  author = {Barthe, Gilles and Gr\'egoire, Benjamin and Pastawski, Fernando},
  title = {{CIC$\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions}},
  booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning, Proceedings},
  series = {Lecture Notes in Artificial Intelligence},
  year = 2006,
  volume = {4246},
  pages = {257--271},
  publisher = {Springer-Verlag Berlin Heidelberg},
  doi = {10.1007/11916277\_18},
  issn = {0302-9743},
  isbn = {3-540-48281-4}
}

@inproceedings{CIC-hat-minus-nat,
  title = {{On Strong Normalization of the Calculus of Constructions with Type-Based Termination}},
  volume = {6397},
  isbn = {978-3-642-16241-1; 978-3-642-16242-8},
  booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning, Proceedings},
  publisher = {Springer-Verlag Berlin Heidelberg},
  author = {Grégoire, Benjamin and Sacchini, Jorge Luis},
  year = 2010,
  doi = {10.1007/978-3-642-16242-8\_24},
  series = {Lecture Notes in Computer Science},
  pages = {333--347},
}

@incollection{F-hat-times,
  title = {{Type-Based Termination with Sized Products}},
  volume = {5213},
  isbn = {978-3-540-87530-7; 978-3-540-87531-4},
  booktitle = {Computer {Science} {Logic}},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag Berlin Heidelberg},
  author = {Barthe, Gilles and Grégoire, Benjamin and Riba, Colin},
  year = 2008,
  doi = {10.1007/978-3-540-87531-4\_35},
  pages = {493--507},
}

@inproceedings{CIC-hat-l,
  author = {Sacchini, Jorge Luis},
  title = {{Linear Sized Types in the Calculus of Constructions}},
  booktitle = {Functional and Logic Programming},
  series = {Lecture Notes in Computer Science},
  year = 2014,
  volume = {8475},
  pages = {169--185},
  publisher = {Springer-Verlag Berlin Heidelberg},
  doi = {10.1007/978-3-319-07151-0\_11},
  issn = {0302-9743},
  eissn = {1611-3349},
  isbn = {978-3-319-07151-0; 978-3-319-07150-3}
}

@InProceedings{CCE,
  author = {Oury, Nicolas},
  title = {{Extensionality in the Calculus of Constructions}},
  booktitle = {Theorem Proving in Higher Order Logics},
  series = {Lecture Notes in Computer Science},
  volume = {3603},
  year = 2005,
  publisher = {Springer-Verlag Berlin Heidelberg},
  pages = {278--293},
  isbn = {978-3-540-31820-0},
  doi = {10.1007/11541868\_18}
}

@inproceedings{guard,
  title = {{Codifying guarded definitions with recursive schemes}},
  isbn = {978-3-540-47770-9},
  booktitle = {Types for Proofs and Programs},
  series = {Lecture Notes in Computer Science},
  volume = {996},
  publisher = {Springer-Verlag Berlin Heidelberg},
  author = {Giménez, Eduardo},
  year = 1995,
  pages = {39--59},
  doi = {10.1007/3-540-60579-7\_3}
}

@incollection{CCR,
  title = {{Structural recursive definitions in type theory}},
  volume = {1443},
  isbn = {978-3-540-64781-2; 978-3-540-68681-1},
  booktitle = {Automata, Languages and Programming},
  publisher = {Springer-Verlag Berlin Heidelberg},
  author = {Giménez, Eduardo},
  year = 1998,
  doi = {10.1007/BFb0055070},
  series = {Lecture Notes in Computer Science},
  pages = {397--408},
}

@inproceedings{CIC,
  title = {{Inductively defined types in the Calculus of Constructions}},
  volume = {442},
  isbn = {978-0-387-97375-3; 978-0-387-34808-7},
  pages = {209--228},
  booktitle = {Mathematical Foundations of Programming Semantics},
  publisher = {Springer-Verlag Berlin Heidelberg},
  author = {Pfenning, Frank and Paulin-Mohring, Christine},
  year = 1990,
  doi = {10.1007/BFb0040259},
  series = {Lecture Notes in Computer Science}
}

@inproceedings{TemplateCoq,
  title = {{Towards Certified Meta-Programming with Typed Template-Coq}},
  author = {Anand, Abhishek and Boulier, Simon and Cohen, Cyril and Sozeau, Matthieu and Tabareau, Nicolas},
  url = {https://hal.archives-ouvertes.fr/hal-01809681},
  booktitle = {Interactive Theorem Proving},
  publisher = {Springer Cham},
  series = {Lecture Notes in Computer Science},
  volume = {10895},
  pages = {20--39},
  year = 2018,
  month = Jul,
  doi = {10.1007/978-3-319-94821-8\_2},
  isbn = {978-3-319-94820-1}
}

@inproceedings{cc-hat-omega,
  author = {Sacchini, Jorge Luis},
  title = {{Type-Based Productivity of Stream Definitions in the Calculus of Constructions}},
  booktitle = {Logic in Computer Science},
  year = 2013,
  pages = {233-242},
  publisher = {IEEE Computer Society},
  doi = {10.1109/LICS.2013.29},
  issn = {1043-6871},
  isbn = {978-1-4799-0413-6}
}

@InProceedings{typed-NbE,
  author = {Abel, Andreas and Coquand, Thierry and Dybjer, Peter},
  title = {{Normalization by Evaluation for Martin-L\"of Type Theory with Typed Equality Judgements}},
  booktitle = {Logic in Computer Science},
  year = 2007,
  doi = {10.1109/LICS.2007.33},
  publisher = {IEEE Computer Society},
  pages = {3--12},
  isbn = {0-7695-2908-9},
  issn = {1043-6871}
}

@InProceedings{ECC,
  author = {Luo, Zhaohui},
  booktitle = {Logic in Computer Science},
  title = {{ECC, an extended calculus of constructions}},
  publisher = {IEEE Computer Society},
  year = 1989,
  pages = {386--395},
  doi = {10.1109/LICS.1989.39193},
  isbn = {0-8186-1954-6}
}

@inproceedings{guarded-types,
  author = {Nakano, Hiroshi},
  title = {{A Modality for Recursion}},
  year = 2000,
  isbn = {0-7695-0725-5},
  issn = {1043-6871},
  publisher = {IEEE Computer Society},
  pages = {255--266},
  booktitle = {Logic in Computer Science},
  doi = {10.1109/LICS.2000.855774}
}

@inproceedings{MiniAgda,
  title = {{MiniAgda: Integrating Sized and Dependent Types}},
  volume = {43},
  issn = {2075-2180},
  doi = {10.4204/EPTCS.43.2},
  booktitle = {Partiality and Recursion in Interactive Theorem Provers},
  series = {Electronic Proceedings in Theoretical Computer Science},
  publisher = {Open Publishing Association},
  author = {Abel, Andreas},
  year = 2010,
  month = Dec,
  pages = {14--28},
  url = {http://eptcs.web.cse.unsw.edu.au/paper.cgi?PAR2010.2}
}

@incollection{flationary,
  title = {{Type-Based Termination, Inflationary Fixed-Points, and Mixed Inductive-Coinductive Types}},
  volume = {77},
  issn = {2075-2180},
  doi = {10.4204/EPTCS.77.1},
  booktitle = {Fixed Points in Computer Science},
  series = {Electronic Proceedings in Theoretical Computer Science},
  publisher = {Open Publishing Association},
  author = {Abel, Andreas},
  year = 2012,
  month = {Feb},
  pages = {1--11},
  url = {http://eptcs.web.cse.unsw.edu.au/paper.cgi?FICS2012.1}
}

@inproceedings{MetaCoq,
  author = {Sozeau, Matthieu},
  volume = {337},
  booktitle = {Logical Frameworks and Meta-Languages: Theory and Practice},
  series = {Electronic Proceedings in Theoretical Computer Science},
  title = {{Touring the MetaCoq Project}},
  year = 2021,
  month = Jul,
  doi = {10.4204/EPTCS.337.2},
  url = {http://eptcs.web.cse.unsw.edu.au/paper.cgi?LFMTP2021.2}
}

@inproceedings{syntactic-models,
  title = {{The next 700 syntactical models of type theory}},
  author = {Boulier, Simon and P{\'e}drot, Pierre-Marie and Tabareau, Nicolas},
  url = {https://hal.inria.fr/hal-01445835},
  booktitle = {Certified Programs and Proofs},
  publisher = {Association for Computing Machinery},
  pages = {182--194},
  year = 2017,
  month = Jan,
  doi = {10.1145/3018610.3018620}
}

@inproceedings{CICE,
  title = {{Eliminating Reflection from Type Theory}},
  author = {Winterhalter, Th{\'e}o and Sozeau, Matthieu and Tabareau, Nicolas},
  url = {https://hal.archives-ouvertes.fr/hal-01849166},
  booktitle = {Certified Programs and Proofs},
  publisher = {Association for Computing Machinery},
  pages = {91--103},
  year = 2019,
  month = Jan,
  doi = {10.1145/3293880.3294095},
}

@inproceedings{hughes,
  title = {Proving the correctness of reactive systems using sized types},
  isbn = {978-0-89791-769-8},
  doi = {10.1145/237721.240882},
  booktitle = {Principles of Programming Languages},
  publisher = {Association for Computing Machinery},
  author = {Hughes, John and Pareto, Lars and Sabry, Amr},
  month = Jan,
  year = 1996,
  pages = {410--423},
}

@InProceedings{ordinals,
  author = {Kraus, Nicolai and Nordvall Forsberg, Fredrik and Xu, Chuangjie},
  title = {{Connecting Constructive Notions of Ordinals in Homotopy Type Theory}},
  booktitle = {Mathematical Foundations of Computer Science},
  pages = {70:1--70:16},
  series = {Leibniz International Proceedings in Informatics},
  isbn = {978-3-95977-201-3},
  issn = {1868-8969},
  year = 2021,
  volume = {202},
  publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  url = {https://drops.dagstuhl.de/opus/volltexte/2021/14510},
  urn = {urn:nbn:de:0030-drops-145100},
  doi = {10.4230/LIPIcs.MFCS.2021.70},
}

@InProceedings{whynotW,
  author = {Hugunin, Jasper},
  title = {{Why Not W?}},
  booktitle = {Types for Proofs and Programs},
  pages = {8:1--8:9},
  series = {Leibniz International Proceedings in Informatics},
  isbn = {978-3-95977-182-5},
  issn = {1868-8969},
  year = 2021,
  volume = {188},
  publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  url = {https://drops.dagstuhl.de/opus/volltexte/2021/13887},
  urn = {urn:nbn:de:0030-drops-138876},
  doi = {10.4230/LIPIcs.TYPES.2020.8}
}

@InProceedings{ind-ind,
  author = {Kaposi, Ambrus and Kov{\'a}cs, Andr{\'a}s and Lafont, Ambroise},
  title = {{For Finitary Induction-Induction, Induction Is Enough}},
  booktitle = {Types for Proofs and Programs},
  pages = {6:1--6:30},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  isbn = {978-3-95977-158-0},
  issn = {1868-8969},
  year = 2020,
  volume = {175},
  publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  url = {https://drops.dagstuhl.de/opus/volltexte/2020/13070},
  urn = {urn:nbn:de:0030-drops-130707},
  doi = {10.4230/LIPIcs.TYPES.2019.6}
}

@InProceedings{TTGU,
  author =	{Kov\'acs, Andr\'as},
  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},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/15748},
  URN =		{urn:nbn:de:0030-drops-157485},
  doi =		{10.4230/LIPIcs.CSL.2022.28}
}

@inproceedings{guard-relax,
  title = {{A relaxation of Coq's guard condition}},
  author = {Boutillier, Pierre},
  url = {https://hal.archives-ouvertes.fr/hal-00651780},
  booktitle = {Journ{\'e}es Francophones des Langages Applicatifs},
  pages = {1--14},
  year = 2012,
  month = Feb
}

@inproceedings{modal-sizes,
  title = {{Towards Unifying (Co)induction and Structural Control}},
  author = {Somayyajula, Siva},
  url = {https://hal-lirmm.ccsd.cnrs.fr/lirmm-03271428},
  booktitle = {{Trends in Linear Logic and Applications}},
  year = 2021,
  month = Jun
}

@inproceedings{Z,
  author = {Dehornoy, Patrick and van Oostrom, Vincent},
  booktitle = {Logical Models of Reasoning and Computation},
  title = {Z., Proving confluence by monotonic single-step upperbound functions},
  year = {2008},
  month = May,
  url = {http://cl-informatik.uibk.ac.at/users/vincent/research/publication/talk/lmrc060508.pdf}
}

@inproceedings{Idris,
  author = {Brady, Edwin C.},
  booktitle = {Programming Languages Meets Program Verification},
  publisher = {Association for Computing Machinery},
  title = {{\textsc{Idris} --- Systems Programming Meets Full Dependent Types}},
  year = 2011,
  month = Jan,
  doi = {10.1145/1929529.1929536},
  isbn = {9781450304870},
  pages = {43–-54}
}

@inproceedings{Lean,
  author = {de Moura, Leonardo and Kong, Soonho and Avigad, Jeremy and van Doorn, Floris and von Raumer, Jakob},
  booktitle = {International Conference on Automated Deduction},
  title = {{The Lean Theorem Prover (System Description)}},
  year = 2015,
  month = Aug,
  volume = {9195},
  doi = {10.1007/978-3-319-21401-6\_26},
  series = {Lecture Notes in Computer Science},
  isbn = {978-3-319-21400-9, 978-3-319-21401-6},
  pages = {378--388}
}

@inproceedings{F-star,
  author = {Swamy, Nikhil and Hri\c{t}cu, C\u{a}t\u{a}lin and Keller, Chantal and Rastogi, Aseem and Delignat-Lavaud, Antoine and Forest, Simon and Bhargavan, Karthikeyan and Fournet, Cédric and Strub, Pierre-Yves and Kohlweiss, Markulf and Zinzindohoue, Jean-Karim and Zanella-B\'eguelin, Santiago},
  title = {{Dependent Types and Multi-Monadic Effects in F$^*$}},
  booktitle = {Principles of Programming Languages},
  year = 2016,
  month = Jan,
  doi = {10.1145/2837614.2837655},
  pages = {256--270},
  isbn = {978-1-4503-3549-2},
}

% Other conference material

@misc{eta,
  title = {{\`A bas l'$\eta$ --- Coq's troublesome $\eta$-conversion}},
  author = {Lennon-Bertrand, Meven},
  url = {https://popl22.sigplan.org/details/wits-2022-papers/15},
  pdf = {https://www.meven.ac/documents/22-WITS-abstract.pdf},
  institution = {Inria LS2N, Universit\'e de Nantes},
  year = 2021,
  month = Jan
}

@misc{SRC,
  title = {{Towards a Syntactic Model of Sized Dependent Types}},
  author = {Chan, Jonathan},
  url = {https://popl22.sigplan.org/details/POPL-2022-student-research-competition/1/Towards-a-Syntactic-Model-of-Sized-Dependent-Types},
  year = 2022,
  month = Jan
}

% Online resources

@misc{W-types,
  author = {McBride, Conor},
  url = {https://mazzo.li/epilogue/index.html\%3Fp=324.html},
  title = {W-types: good news and bad news},
  year = 2010,
  month = Mar,
  date = 7
}

@misc{infinity,
  title = {{\#2820 Equality is incompatible with sized types}},
  author = {Abel, Andreas},
  year = 2017,
  month = Oct,
  url = {https://github.com/agda/agda/issues/2820}
}

@misc{coind-SR,
  title = {{\#6768 Towards a fix to the loss of subject reduction with corecursion?}},
  author = {Herbelin, Hugo},
  year = 2018,
  month = Feb,
  url = {https://github.com/coq/coq/issues/6768}
}

@misc{coqterm,
  author = {{Coq Development Team}, The},
  title = {{CoqTerminationDiscussion}},
  year = 2017,
  url = {https://github.com/coq/coq/wiki/CoqTerminationDiscussion}
}

@misc{palette,
  author = {Okabe, Masataka and Ito, Kei},
  title = {{Color Universal Design (CUD): How to make figures and presentations that are friendly to Colorblind people}},
  year = 2002,
  month = Nov,
  date = 20,
  url = {https://jfly.uni-koeln.de/color/},
}

@misc{Coq,
  author = {{Coq Development Team}, The},
  title = {{The Coq Proof Assistant}},
  month = Jan,
  year = 2022,
  publisher = {Zenodo},
  version = {8.15},
  doi = {10.5281/zenodo.5846982},
  url = {https://coq.github.io/doc/v8.15/refman}
}

@misc{Coq-manual,
  author = {{Coq Development Team}, The},
  title = {{The Coq Proof Assistant Reference Manual}},
  version = {8.4pl6},
  year = 2014,
  url = {https://coq.inria.fr/distrib/V8.4pl6/refman/}
}

% Preprints

@unpublished{CIC-hat-sub,
  title = {{Well-Founded Sized Types in the Calculus of (Co)Inductive Constructions}},
  author = {Sacchini, Jorge Luis},
  year = 2015,
  url = {https://web.archive.org/web/20160606143713/http://www.qatar.cmu.edu/~sacchini/well-founded/well-founded.pdf},
  note = {Unpublished paper}
}

@unpublished{CIC-hat-star,
  title = {{Is Sized Typing for Coq Practical?}},
  author = {Chan, Jonathan and Li, Yufeng and Bowman, William J.},
  year = 2021,
  url = {https://arxiv.org/abs/1912.05601},
  note = {Preprint}
}