references.yaml

exception-model:
  type: article
  title: "Failure is Not an Option: An Exceptional Type Theory"
  page-range: 245-271
  author:
    - Pédrot, Pierre-Marie
    - Tabareau, Nicolas
  parent:
    # - type: conference
    #   title: 27th European Symposium on Programming
    #   location: Thessaloniki, Greece
    - type: conference
      title: Lecture Notes in Computer Science
      volume: 10801
      date: 2018
  serial-number:
    doi: 10.1007/978-3-319-89884-1_9

exception-agda:
  type: repository
  author: Kovács, András
  title: Antifunext
  date: 2024
  url: https://github.com/AndrasKovacs/antifunext
  note: GitHub repository

polynomial-agda:
  type: repository
  author: Kovács, András
  title: Polynomial model
  date: 2020
  url: https://github.com/AndrasKovacs/polynomial-model
  note: GitHub repository

mltt-1971:
  type: misc
  author: Martin-Löf, Per
  title: A Theory of Types
  date: 1971
  url: "https://github.com/michaelt/martin-lof/blob/master/pdfs/martin-loef1971%20-%20A%20Theory%20of%20Types.pdf"
  note: Unpublished manuscript

stlc-sum-eta:
  type: misc
  author: Scherer, Gabriel
  title: Deciding equivalence with sums and the empty type
  date: 2016
  note: ArXiv preprint
  serial-number:
    doi: 10.48550/arXiv.1610.01213

lean-con-ch:
  type: article
  author:
    - Han, Jesse Michael
    - van Doorn, Floris
  title: A formal proof of the independence of the continuum hypothesis
  date: 2020
  parent:
    type: proceedings
    title: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs

natural-model:
  type: misc
  author: Awodey, Steve
  title: Natural models of homotopy type theory
  date: 2017
  note: ArXiv preprint
  serial-number:
    doi: 10.48550/arXiv.1406.3219

gs-framework:
  type: misc
  title: 'Syntactic categories for dependent type theory: sketching and adequacy'
  author:
  - Gratzer, Daniel
  - Sterling, Jonathan
  date: 2021
  note: ArXiv preprint
  serial-number:
    doi: 10.48550/arXiv.2012.10783


girard-paradox:
  type: thesis
  note: Doctoral dissertation
  author: Girard, Jean-Yves
  title: Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur
  date: 1972
  url: https://girard.perso.math.cnrs.fr/These.pdf

on-cubism:
  type: article
  author: Jacobs, Bart
  title: On Cubism
  date: 1996
  page-range: 379-392
  parent:
    title: Journal of Functional Programming
    volume: 6
    issue: 3
    publisher: Cambridge University Press

hurkens-paradox:
  type: article
  title: A simplification of Girard’s paradox
  author: Hurkens, Antonius J. C.
  date: 1995
  page-range: 266-278
  serial-number:
    doi: 10.1007/BFb0014058
  parent:
    - type: conference
      title: Lecture Notes in Computer Science
      volume: 902
    # - type: proceedings
    #   title: Typed Lambda Calculi and Applications

impredicative-sigma:
  type: report
  title: Impredicative Strong Existential Equivalent to $"Type":"Type"$
  author:
    - Hook, James G.
    - Howe, Douglas J.
  date: 1986
  serial-number:
    doi: 10.5555/866154

elim-pattern-matching:
  type: article
  title: Eliminating Dependent Pattern Matching
  author:
    - Goguen, Healfdene
    - McBride, Conor
    - McKinna, James
  date: 2006
  page-range: 521-540
  serial-number:
    doi: 10.1007/11780274_27
  parent:
    - type: book
      title: Algebra, Meaning, and Computation
      publisher: Springer, Berlin, Heidelberg

elim-pattern-matching-without-K:
  type: article
  title: Eliminating dependent pattern matching without K
  author:
    - Cockx, Jesper
    - Devriese, Dominique
    - Piessens, Frank
  date: 2016
  page-range: e16
  parent:
    title: Journal of Functional Programming
    volume: 26
    publisher: Cambridge University Press
  serial-number:
    doi: 10.1017/S0956796816000174

independence-results-coc:
  type: article
  author: Streicher, Thomas
  title: Independence results for calculi of dependent types
  date: 1989
  serial-number:
    doi: 10.1007/BFb0018350
  page-range: 141-154
  parent:
    type: book
    title: Category Theory and Computer Science
    volume: 389
    publisher: Springer, Berlin, Heidelberg

groupoid-interpretation:
  type: article
  title: The groupoid interpretation of type theory
  author:
    - Hofmann, Martin
    - Streicher, Thomas
  date: 1996
  parent:
    type: book
    title: Twenty-five years of constructive type theory
    volume: 36
  page-range: 83-111
  url: https://ncatlab.org/nlab/files/HofmannStreicherGroupoidInterpretation.pdf

inf-groupoid-homotopy-type:
  type: article
  title: $infinity$-groupoids and homotopy types
  author:
    - Kapranov, M. M.
    - Voevodsky, V. A.
  date: 1991
  page-range: 29-46
  parent:
    title: Cahiers de Topologie et Géométrie Différentielle Catégoriques
    volume: 32
    issue: 1
  url: https://eudml.org/doc/91469

homotopy-type-3-groupoid:
  type: misc
  note: ArXiv preprint
  title: Homotopy types of strict 3-groupoids
  author: Simpson, Carlos
  date: 1998
  serial-number:
    doi: 10.48550/arXiv.math/9810059

simplicial-model:
  type: misc
  note: ArXiv preprint
  title: The Simplicial Model of Univalent Foundations (after Voevodsky)
  author:
    - Kapulkin, Chris
    - Lumsdaine, Peter LeFanu
  date: 2012
  serial-number:
    doi: 10.48550/arXiv.1211.2851

hott-book:
  type: book
  title: "Homotopy Type Theory: Univalent Foundations of Mathematics"
  author: The Univalent Foundations Program
  date: 2013
  url: https://homotopytypetheory.org/book/

type-theory-book:
  type: book
  title: Principles of Dependent Type Theory
  author:
    - Anguili, Carlo
    - Gratzer, Daniel
  note: In preparation
  url: https://www.danielgratzer.com/papers/type-theory-book.pdf

synthetic-computability:
  type: article
  title: First Steps in Synthetic Computability Theory
  date: 2006
  author: Bauer, Andrej
  page-range: 5-31
  parent:
    - type: periodical
      title: Electronic Notes in Theoretical Computer Science
      volume: 155
    # - type: conference
    #   title: Proceedings of the 21st Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXI)
  serial-number:
    doi: 10.1016/j.entcs.2005.11.049

comprehension-type-theory:
  type: misc
  note: ArXiv preprint
  title: A Type Theory for Comprehension Categories with Applications to Subtyping
  author:
    - Najmaei, Niyousha
    - vd. Weide, Niels
    - Ahrens, Benedikt
    - North, Paige Randall
  date: 2025
  serial-number:
    doi: 10.48550/arXiv.2503.10868

mtt-thesis:
  type: thesis
  note: Doctoral dissertation
  title: Syntax and semantics of modal type theory
  author: Gratzer, Daniel
  date: 2023
  url: https://www.danielgratzer.com/papers/phd-thesis.pdf

clans-and-tribes:
  type: misc
  note: ArXiv preprint
  title: Notes on Clans and Tribes
  author: Joyal, Andre
  date: 2017
  serial-number:
    doi: 10.48550/arXiv.1710.10238

seely-lccc:
  type: article
  title: Locally cartesian closed categories and type theory
  date: 1984
  page-range: 33-48
  author: Seely, R. A. G.
  parent:
    title: Mathematical Proceedings of the Cambridge Philosophical Society
    volume: 95
    issue: 1
  serial-number:
    doi: 10.1017/S0305004100061284

bocquet-strictification:
  type: article
  title: Strictification of Weakly Stable Type-Theoretic Structures Using Generic Contexts
  author: Bocquet, Rafaël
  date: 2022
  page-range: 1-23
  serial-number:
    doi: 10.4230/LIPIcs.TYPES.2021.3
  parent:
    type: proceedings
    title: 27th International Conference on Types for Proofs and Programs (TYPES 2021)
    volume: 239
    parent:
      type: proceedings
      title: Leibniz International Proceedings in Informatics (LIPIcs)

dialectica:
  type: article
  title: Dialectica models of type theory
  author:
  - Moss, Sean K.
  - name: Glehn
    given-name: Tamara
    prefix: von
  date: 2018
  page-range: 739-748
  serial-number:
    doi: 10.1145/3209108.3209207
    isbn: '9781450355834'
  parent:
    type: proceedings
    title: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science
    publisher:
      name: Association for Computing Machinery
      location: Oxford, United Kingdom
    parent:
      type: proceedings
      title: LICS '18

polynomial-model:
  type: thesis
  title: Polynomials and models of type theory
  author: Von Glehn, Tamara
  date: 2015
  school: University of Cambridge
  note: PhD thesis
  serial-number:
    doi: 10.17863/CAM.16245

univalence-without-funext:
  type: misc
  note: ArXiv preprint
  title: Univalence without function extensionality
  author:
  - Cavallo, Evan
  - Höfer, Jonas
  date: 2026
  serial-number:
    doi: 10.48550/arXiv.2605.00812

container-model:
  type: misc
  title: A container model of type theory
  author:
  - Altenkirch, Thorsten
  - Kaposi, Ambrus
  date: 2021
  note: Talk at TYPES 2021.

hofmann-coherence:
  type: article
  title: On the Interpretation of Type Theory in Locally Cartesian Closed Categories
  author: Hofmann, Martin
  date: 1994
  page-range: 427-441
  parent:
    type: proceedings
    title: Selected Papers from the 8th International Workshop on Computer Science Logic
    publisher:
      name: Springer-Verlag
      location: Berlin, Heidelberg
    parent:
      type: proceedings
      title: CSL '94

curien-coherence:
  type: article
  title: Substitution up to isomorphism
  author: Curien, Pierre-Louis
  date: 1993-09
  page-range: 51-85
  serial-number:
    issn: 0169-2968
  parent:
    type: periodical
    title: Fundamenta Informaticae
    publisher:
      name: IOS Press
      location: NLD
    issue: 1–2
    volume: 19

clairambault:
  type: article
  title: The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories
  author:
  - Clairambault, Pierre
  - Dybjer, Peter
  date: 2014-04
  serial-number:
    doi: 10.1017/s0960129513000881
  parent:
    type: periodical
    title: Mathematical Structures in Computer Science
    publisher: Cambridge University Press (CUP)
    issue: 6
    volume: 24

local-universes:
  type: article
  title: 'The Local Universes Model: An Overlooked Coherence Construction for Dependent Type Theories'
  author:
  - Lumsdaine, Peter Lefanu
  - Warren, Michael A.
  date: 2015-07
  page-range: 1-31
  serial-number:
    doi: 10.1145/2754931
  parent:
    type: periodical
    title: ACM Transactions on Computational Logic
    publisher: Association for Computing Machinery (ACM)
    issue: 3
    volume: 16

general-framework:
  type: article
  title: A general framework for the semantics of type theory
  author: Uemura, Taichi
  date: 2023-03
  page-range: 134-179
  serial-number:
    doi: 10.1017/s0960129523000208
    issn: 1469-8072
  parent:
    type: periodical
    title: Mathematical Structures in Computer Science
    publisher: Cambridge University Press (CUP)
    issue: 3
    volume: 33

sterling-thesis:
  type: thesis
  title: 'First Steps in Synthetic {Tait} Computability: The Objective Metatheory of Cubical Type Theory'
  author: Sterling, Jonathan
  date: 2021
  organization: Carnegie Mellon University
  issue: CMU-CS-21-142
  serial-number:
    doi: 10.5281/zenodo.6990769
  note: PhD thesis

functorial-semantics:
  type: article
  title: Functorial Semantics Of Algebraic Theories
  author: Lawvere, F. William
  date: 1963-11
  page-range: 869-872
  serial-number:
    doi: 10.1073/pnas.50.5.869
    issn: 1091-6490
  parent:
    type: periodical
    title: Proceedings of the National Academy of Sciences
    publisher: National Academy of Sciences
    issue: 5
    volume: 50

pfpl:
  type: book
  title: Practical Foundations for Programming Languages
  author: Harper, Robert
  date: 2016
  publisher: Cambridge University Press
  url: https://www.cs.cmu.edu/~rwh/pfpl.html

meaning-explanation:
  type: article
  title: Constructive Mathematics and Computer Programming
  author: Martin-Löf, Per
  date: 1982
  editor:
  - Cohen, L. Jonathan
  - Łoś, Jerzy
  - Pfeiffer, Helmut
  - Podewski, Klaus-Peter
  page-range: 153-175
  serial-number:
    doi: 10.1016/S0049-237X(09)70189-2
    issn: 0049-237X
  parent:
    type: book
    title: Logic, Methodology and Philosophy of Science VI
    publisher: Elsevier
    volume: 104

nuprl-book:
  type: book
  title: Implementing Mathematics with the {NuPRL} Proof Development System
  author:
  - Constable, Robert L.
  - Allen, Stuart F.
  - Bromley, H. M.
  - Cleaveland, W. R.
  - Cremer, J. F.
  - Harper, R. W.
  - Howe, Douglas J.
  - Knoblock, T. B.
  - Mendler, N. P.
  - Panangaden, P.
  - Sasaki, James T.
  - Smith, Scott F.
  date: 1986
  publisher:
    name: Prentice-Hall
    location: New Jersey

js-meaning-explanation:
  type: misc
  note: ArXiv preprint
  title: Type Theory and its Meaning Explanations
  author: Sterling, Jonathan
  date: 2016
  serial-number:
    doi: 10.48550/arXiv:1512.01837

domain-theory-inversion:
  type: misc
  note: ArXiv preprint
  title: Definitional Inversion, Without Normalisation
  author:
    - Carneiro, Mario
    - Coquand, Thierry
    - Mathieu, Adrien Frabetti
    - Lennon-Bertrand, Meven
    - Melliès, Paul-André
    - Weirich, Stephanie
  date: 2026
  serial-number:
    doi: 10.48550/arXiv:2607.13662

syntactic-models:
  type: article
  title: The next 700 syntactical models of type theory
  author:
  - Boulier, Simon
  - Pédrot, Pierre-Marie
  - Tabareau, Nicolas
  date: 2017-01
  page-range: 182-194
  serial-number:
    doi: 10.1145/3018610.3018620
  parent:
    type: proceedings
    title: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs
    publisher: ACM
    parent:
      type: proceedings
      title: CPP '17