@unpublished{martinlof1972,
  author = {Per Martin-L{\"o}f},
  title = {An Intuitionistic Theory of Types},
  year = {1972},
  note = {Manuscript},
  url = {https://archive-pml.github.io/martin-lof/pdfs/An-Intuitionistic-Theory-of-Types-1972.pdf}
}
@inproceedings{brady2021,
  author = {Edwin Brady},
  title = {Idris 2: Quantitative Type Theory in Practice},
  booktitle = {ECOOP},
  year = {2021},
  url = {https://arxiv.org/abs/2104.00480}
}
@inproceedings{swamy2016,
  author = {Nikhil Swamy and others},
  title = {Dependent Types and Multi-monadic Effects in F*},
  booktitle = {POPL},
  year = {2016},
  url = {https://fstar-lang.org/papers/mumon/paper.pdf}
}
@misc{leanvalidation,
  author = {{Lean project}},
  title = {Validating a Lean Proof},
  note = {Accessed 2026-09-25},
  url = {https://lean-lang.org/doc/reference/latest/ValidatingProofs/}
}
@misc{mlirreference,
  author = {{LLVM project}},
  title = {MLIR Language Reference},
  note = {Accessed 2026-09-25},
  url = {https://mlir.llvm.org/docs/LangRef/}
}
@inproceedings{chlipala2015,
  author = {Adam Chlipala},
  title = {Ur/Web: A Simple Model for Programming the Web},
  booktitle = {POPL},
  year = {2015},
  url = {https://adam.chlipala.net/papers/UrWebPOPL15/UrWebPOPL15.pdf}
}