% quantitative stuff

@inproceedings{grtt,
  author    = {Moon, Benjamin and Eades, III, Harley and Orchard, Dominic},
  editor    = {Yoshida, Nobuko},
  title     = {Graded Modal Dependent Type Theory},
  booktitle = {Programming Languages and Systems:
               European Symposium on Programming ({ESOP})},
  series    = {Lecture Notes in Computer Science},
  volume    = {12648},
  pages     = {462--490},
  publisher = {Springer},
  year      = {2021},
  url       = {https://doi.org/10.1007/978-3-030-72019-3\_17},
  doi       = {10.1007/978-3-030-72019-3\_17}
}

@inproceedings{nuttin,
  author    = {Conor McBride},
  editor    = {Sam Lindley and Conor McBride and
               Philip W. Trinder and Donald Sannella},
  title     = {I Got Plenty o' Nuttin'},
  booktitle = {A List of Successes That Can Change the World---Essays Dedicated
               to {P}hilip {W}adler on the Occasion of His 60th Birthday},
  pages     = {207--233},
  publisher = {Springer},
  year      = {2016},
% url       = {https://doi.org/10.1007/978-3-319-30936-1\_12},
  url       = {https://personal.cis.strath.ac.uk/conor.mcbride/PlentyO-CR.pdf},
}

@inproceedings{qtt,
  author    = {Robert Atkey},
  editor    = {Anuj Dawar and
               Erich Grädel},
  title     = {Syntax and Semantics of Quantitative Type Theory},
  booktitle = {Logic in Computer Science ({LICS})},
  pages     = {56--65},
  publisher = {{ACM}},
  year      = {2018},
% url       = {https://doi.org/10.1145/3209108.3209189},
  url       = {https://bentnib.org/quantitative-type-theory.pdf}
}


% observational stuff

@inproceedings{ott-now,
  author    = {Thorsten Altenkirch and Conor McBride and Wouter Swierstra},
  editor    = {Aaron Stump and Hongwei Xi},
  title     = {Observational equality, now!},
  booktitle = {Programming Languages meets Program Verification ({PLPV})},
  publisher = {{ACM}},
  year      = {2007},
  url       = {https://www.cs.nott.ac.uk/~psztxa/publ/obseqnow.pdf},
}

@inproceedings{ott-good,
  author    = {Loïc Pujet and Nicolas Tabareau},
  title     = {Observational equality: now for good},
  booktitle = {Principles of Programming Languages ({POPL})},
  pages     = {1--27},
  year      = {2022},
  url       = {https://doi.org/10.1145/3498693},
  doi       = {10.1145/3498693},
}

@inproceedings{xtt,
  author    = {Jonathan Sterling and Carlo Angiuli and Daniel Gratzer},
  editor    = {Herman Geuvers},
  title     = {Cubical Syntax for Reflection-Free Extensional Equality},
  booktitle = {Formal Structures for Computation and Deduction ({FSCD})},
  series    = {LIPIcs},
  volume    = {131},
  pages     = {31:1--31:25},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  year      = {2019},
% url       = {https://doi.org/10.4230/LIPIcs.FSCD.2019.31},
  url       = {https://arxiv.org/pdf/1904.08562.pdf},
  doi       = {10.4230/LIPIcs.FSCD.2019.31}
}


% Misc type stuff

@misc{crude,
  author = {McBride, Conor},
  title  = {Crude but effective stratification (slides)},
  url    = {https://personal.cis.strath.ac.uk/conor.mcbride/Crude.pdf},
  note   = {Slides}
}

@misc{crude-blog,
  author = {McBride, Conor},
  title  = {Crude but Effective Stratification},
  url    = {https://mazzo.li/epilogue/index.html%3Fp=857&cpage=1.html},
  year   = {2011},
}

@inproceedings{mugen,
  author    = {Hou (Favonia), Kuen-Bang and Angiuli, Carlo and Mullanix, Reed},
  title     = {An Order-Theoretic Analysis of Universe Polymorphism},
  month     = {jan},
  year      = {2023},
  url       = {https://doi.org/10.1145/3571250},
  doi       = {10.1145/3571250},
  booktitle = {Principles of Programming Languages ({POPL})},
}

@article{bidi,
  author    = {Jana Dunfield and Neel Krishnaswami},
  title     = {Bidirectional Typing},
  journal   = {{ACM} Computing Surveys},
  volume    = {54},
  number    = {5},
  year      = {2022},
  url       = {https://doi.org/10.1145/3450952},
  doi       = {10.1145/3450952},
}


% Misc implementation

@article{expl-sub,
  author    = {Martín Abadi and Luca Cardelli and
               Pierre{-}Louis Curien and Jean{-}Jacques Lévy},
  title     = {Explicit Substitutions},
  journal   = {Journal of Functional Programming},
  volume    = {1},
  number    = {4},
  pages     = {375--416},
  year      = {1991},
  url       = {http://lucacardelli.name/Papers/ExplicitSub.pdf}
}

% historical

@inproceedings{indices,
  author       = {Edwin C. Brady and Conor McBride and James McKinna},
  editor       = {Stefano Berardi and Mario Coppo and Ferruccio Damiani},
  title        = {Inductive Families Need Not Store Their Indices},
  booktitle    = {Types for Proofs and Programs ({TYPES})},
  series       = {Lecture Notes in Computer Science},
  volume       = {3085},
  pages        = {115--129},
  publisher    = {Springer},
  year         = {2003},
  url          = {https://doi.org/10.1007/978-3-540-24849-1\_8},
  doi          = {10.1007/978-3-540-24849-1\_8},
  note = {\textit{i couldn't find a non-paywalled version, sorry!
          but it's mostly for historical interest anyway}}
}

% blog post specific
@misc{nlab-wtype,
  author = {{nLab authors}},
  title = {{W}-type},
  howpublished = {\url{https://ncatlab.org/nlab/show/W-type}},
  note = {\href{https://ncatlab.org/nlab/revision/W-type/47}{revision 47}},
  month = nov,
  year = 2023
}

@book{martinlof84,
  author    = {Per Martin-Löf},
  title     = {Intuitionistic type theory},
  series    = {Studies in proof theory},
  volume    = {1},
  publisher = {Bibliopolis},
  year      = {1984},
  isbn      = {978-88-7088-228-5},
  url       = {https://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-retypeset-1984.pdf}
}

% bullshit

@misc{hotminute,
  author = {{Wiktionary}},
  title = {Hot minute},
  year = {2023},
  url = {https://en.wiktionary.org/wiki/hot_minute},
}