@book{barendregt-et-al-2013,
  author    = {Hendrik Pieter Barendregt and
               Wil Dekkers and
               Richard Statman},
  title     = {Lambda Calculus with Types},
  series    = {Perspectives in logic},
  publisher = {Cambridge University Press},
  year      = {2013},
  url       = {http://www.cambridge.org/de/academic/subjects/mathematics/logic-categories-and-sets/lambda-calculus-types},
  isbn      = {978-0-521-76614-2},
  timestamp = {Wed, 12 Mar 2014 19:34:31 +0100},
  biburl    = {https://dblp.org/rec/bib/books/daglib/0032840},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@book{pierce-2002,
  author    = {Benjamin C. Pierce},
  title     = {Types and Programming Languages},
  publisher = {{MIT} Press},
  year      = {2002},
  isbn      = {978-0-262-16209-8},
  timestamp = {Thu, 03 Feb 2011 10:51:35 +0100},
  biburl    = {https://dblp.org/rec/bib/books/daglib/0005958},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{hindley-1969,
  author = "Hindley, J. Roger",
  year = 1969,
  title = "The Principal Type-Scheme of an Object in Combinatory Logic",
  journal = "Trans. Amer. Math. Soc.",
  volume = 146,
  pages = "29--60",
  note = {\url{https://www.jstor.org/stable/pdf/1995158.pdf?casa_token=zeSppXjXzUsAAAAA:fzvl6NKVjcL0iVXjyrMSbh_bq0sxtY4iPeoX5NMC6FvlOdMDxYG1p-aIiqrc6P2Q7UTaT46PVHByMTWrpox4SKwOhbcxjLIm-FxWRDx-FtdyWwHa0ueG}}
}

@article{milner-1978,
  author    = {Robin Milner},
  title     = {A Theory of Type Polymorphism in Programming},
  journal   = {J. Comput. Syst. Sci.},
  volume    = {17},
  number    = {3},
  pages     = {348--375},
  year      = {1978},
  note = {\url{https://www.sciencedirect.com/science/article/pii/0022000078900144/pdf?md5=cdcf7cdb7cfd2e1e4237f4f779ca0df7&pid=1-s2.0-0022000078900144-main.pdf&_valck=1}},
  xxxurl       = {https://doi.org/10.1016/0022-0000(78)90014-4},
  xxxdoi       = {10.1016/0022-0000(78)90014-4},
}

@article{perlis-1982,
  author    = {Alan J. Perlis},
  title     = {Epigrams on Programming},
  journal   = {{SIGPLAN} Notices},
  volume    = {17},
  number    = {9},
  pages     = {7--13},
  year      = {1982},
  XXXurl       = {https://doi.org/10.1145/947955.1083808},
  note = "\url{https://dl.acm.org/doi/pdf/10.1145/947955.1083808?casa_token=Z_grmOD_yAYAAAAA:dvMu7thQc-8XmGJCZ1ARQ24_XB1qel3M1jYUmBPAKfuBaZrryxmKiKValMrwpunJ0dv9vhr2kDvMxA}",
  doi       = {10.1145/947955.1083808},
  timestamp = {Wed, 14 Nov 2018 10:29:14 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/sigplan/Perlis82},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@book{lean-reference-manual,
  title = "The {L}ean 4 Manual",
  XXXauthor = "Jeremy Avigad and Gabriel Ebner and Sebastian Ullrich",
  note = "\url{https://leanprover.github.io/lean4/doc/}",
  year = 2021
}

@book{theorem-proving-in-lean,
  title = "Theorem Proving in {L}ean 4",
  author = "Jeremy Avigad, Leonardo de Moura, Soonho Kong and Sebastian Ullrich",
  note = "\url{https://leanprover.github.io/theorem_proving_in_lean4/}",
  year = 2021}

@book{programming-in-lean,
  title = "Programming in {L}ean",
  author = "Jeremy Avigad and Leonardo de Moura and Jared Roesch",
  note = "\url{https://leanprover.github.io/programming_in_lean/}",
  year = 2016}

@book{van-raamsdonk-2011,
  title = "Logical Verification: Course Notes",
  author = "\raamsdonk, Femke",
  note = "\url{https://www.cs.vu.nl/~jbe248/lv2017/notes.pdf}",
  year = 2011
}

@book{nederpelt-geuvers-2014,
  title = "Type Theory and Formal Proof: An Introduction",
  author = "Rob Nederpelt and Herman Geuvers",
  year = 2014,
  publisher = "Cambridge University Press"
}

@book{osullivan-et-al-2008,
  title = "Real World {H}askell",
  author = "Bryan O'Sullivan and Donald Stewart and John Goerzen",
  publisher = "O'Reilly",
  year = 2008,
  note = "\url{http://book.realworldhaskell.org/read/}"}

@article{ebner-et-al-2017,
  author    = {Gabriel Ebner and
               Sebastian Ullrich and
               Jared Roesch and
               Jeremy Avigad and
               Leonardo de Moura},
  title     = {A metaprogramming framework for formal verification},
  journal   = {{PACMPL}},
  volume    = {1},
  number    = {{ICFP}},
  pages     = {34:1--34:29},
  year      = {2017},
  note = {\url{https://leanprover.github.io/papers/tactic.pdf}},
  XXXurl       = {https://doi.org/10.1145/3110278},
  XXXdoi       = {10.1145/3110278}
}

@book{nipkow-klein-2014,
  author    = {Tobias Nipkow and
               Gerwin Klein},
  title     = {Concrete Semantics: With Isabelle/HOL},
  publisher = {Springer},
  year      = {2014},
  note      = {\url{http://www.concrete-semantics.org/concrete-semantics.pdf}},
  url       = {https://doi.org/10.1007/978-3-319-10542-0},
  doi       = {10.1007/978-3-319-10542-0},
  isbn      = {978-3-319-10541-3},
}

@inproceedings{gonthier-et-al-2013,
  author    = {Georges Gonthier and
               Andrea Asperti and
               Jeremy Avigad and
               Yves Bertot and
               Cyril Cohen and
               Fran{\c{c}}ois Garillot and
               St{\'{e}}phane Le Roux and
               Assia Mahboubi and
               Russell O'Connor and
               Sidi Ould Biha and
               Ioana Pasca and
               Laurence Rideau and
               Alexey Solovyev and
               Enrico Tassi and
               Laurent Th{\'{e}}ry},
  editor    = {Sandrine Blazy and
               Christine Paulin{-}Mohring and
               David Pichardie},
  title     = {A Machine-Checked Proof of the {O}dd {O}rder {T}heorem},
  booktitle = {ITP 2013},
  series    = {Lecture Notes in Computer Science},
  volume    = {7998},
  pages     = {163--179},
  publisher = {Springer},
  year      = {2013},
  note = {\url{https://hal.inria.fr/hal-00816699/document}},
  XXXurl       = {https://doi.org/10.1007/978-3-642-39634-2\_14},
  XXXdoi       = {10.1007/978-3-642-39634-2\_14},
}

@article{gonthier-2008,
  title = "Formal Proof---the {F}our-{C}olor {T}heorem",
  author = "Georges Gonthier",
  journal = "Notices AMS",
  volume = 55,
  number = 11,
  pages = "1382--1393",
  year = 2008,
  note = {\url{https://www.ams.org/notices/200811/tx081101382p.pdf}}}

@article{hales-et-al-2015,
  author    = {Thomas C. Hales and
               Mark Adams and
               Gertrud Bauer and
               Dat Tat Dang and
               John Harrison and
               Truong Le Hoang and
               Cezary Kaliszyk and
               Victor Magron and
               Sean McLaughlin and
               Thang Tat Nguyen and
               Truong Quang Nguyen and
               Tobias Nipkow and
               Steven Obua and
               Joseph Pleso and
               Jason Rute and
               Alexey Solovyev and
               An Hoai Thi Ta and
               Trung Nam Tran and
               Diep Thi Trieu and
               Josef Urban and
               Ky Khac Vu and
               Roland Zumkeller},
  title     = {A formal proof of the {K}epler conjecture},
  journal   = {CoRR},
  volume    = {abs/1501.02155},
  year      = {2015},
  note       = {\url{http://arxiv.org/abs/1501.02155}},
}

@inproceedings{harrison-2003,
  author    = {John Harrison},
  title     = {Formal Verification at {I}ntel},
  booktitle = {LICS 2003},
  pages     = {45--54},
  year      = {2003},
  publisher = {{IEEE} Computer Society},
  note = {\url{https://ieeexplore.ieee.org/document/1210044}}
}

@article{russinoff-1999,
  author    = {David M. Russinoff},
  title     = {A Mechanically Checked Proof of Correctness of the {AMD} {K5} Floating
               Point Square Root Microcode},
  journal   = {Formal Methods in System Design},
  volume    = {14},
  number    = {1},
  pages     = {75--125},
  year      = {1999},
  note = {\url{https://link.springer.com/content/pdf/10.1023/A:1008669628911.pdf}}
}

@article{klein-et-al-2010,
  author    = {Gerwin Klein and
               June Andronick and
               Kevin Elphinstone and
               Gernot Heiser and
               David Cock and
               Philip Derrin and
               Dhammika Elkaduwe and
               Kai Engelhardt and
               Rafal Kolanski and
               Michael Norrish and
               Thomas Sewell and
               Harvey Tuch and
               Simon Winwood},
  title     = {{seL4}: Formal verification of an operating-system kernel},
  journal   = {Commun.\ ACM},
  volume    = {53},
  number    = {6},
  year      = {2010},
  pages     = {107--115},
  note = {\url{https://www.researchgate.net/profile/Gernot_Heiser/publication/220910193_SeL4_Formal_verification_of_an_OS_kernel/links/09e4150f00292a0329000000/SeL4-Formal-verification-of-an-OS-kernel.pdf}}
}

@inproceedings{gu-et-al-2016,
  author    = {Ronghui Gu and
               Zhong Shao and
               Hao Chen and
               Xiongnan (Newman) Wu and
               Jieung Kim and
               Vilhelm Sj{\"{o}}berg and
               David Costanzo},
  editor    = {Kimberly Keeton and
               Timothy Roscoe},
  title     = {{CertiKOS}: An Extensible Architecture for Building Certified Concurrent
               {OS} Kernels},
  booktitle = {{OSDI} 2016},
  pages     = {653--669},
  publisher = {{USENIX} Association},
  year      = {2016},
  note       = {\url{https://www.usenix.org/system/files/conference/osdi16/osdi16-gu.pdf}},
}

@article{leroy-2009-jar,
  author    = {Xavier Leroy},
  title     = {A Formally Verified Compiler Back-end},
  journal   = {J. Automated Reasoning},
  volume    = {43},
  number    = {4},
  year      = {2009},
  pages     = {363--446},
  note = {\url{https://arxiv.org/pdf/0902.2137.pdf}}
}

@inproceedings{lochbihler-2010,
  author    = {Andreas Lochbihler},
  editor    = {Andrew D. Gordon},
  title     = {Verifying a Compiler for {J}ava Threads},
  booktitle = {{ESOP} 2010},
  series    = {Lecture Notes in Computer Science},
  volume    = {6012},
  pages     = {427--447},
  publisher = {Springer},
  year      = {2010},
  note      = {\url{https://link.springer.com/content/pdf/10.1007/978-3-642-11957-6_23.pdf}},
  xxxurl       = {https://doi.org/10.1007/978-3-642-11957-6\_23},
  xxxdoi       = {10.1007/978-3-642-11957-6\_23},
  xxxtimestamp = {Tue, 14 May 2019 10:00:41 +0200},
  xxxbiburl    = {https://dblp.org/rec/bib/conf/esop/Lochbihler10},
  xxxbibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{selsam-de-moura-2016,
  author    = {Daniel Selsam and
               Leonardo de Moura},
  editor    = {Nicola Olivetti and
               Ashish Tiwari},
  title     = {Congruence Closure in Intensional Type Theory},
  booktitle = {{IJCAR} 2016},
  series    = {Lecture Notes in Computer Science},
  volume    = {9706},
  pages     = {99--115},
  publisher = {Springer},
  year      = {2016},
  XXXdoi    = {10.1007/978-3-319-40229-1\_8},
  note = {\url{https://arxiv.org/pdf/1701.04391.pdf}}
}

@inproceedings{mathlib-mathlib-2020,
  title = "The {L}ean Mathematical Library",
  author = "\mathlibcommunity",
  editor = "Jasmin Blanchette and C\u{a}t\u{a}lin Hri\cb{t}cu",
  booktitle = "CPP 2020",
  publisher = "ACM",
  pages = "367--381",
  year = 2020,
  note = {\url{https://arxiv.org/pdf/1910.09336.pdf}}}

@incollection{harrison-et-al-2014,
  author    = {John Harrison and
               Josef Urban and
               Freek Wiedijk},
  editor    = {J{\"{o}}rg H. Siekmann},
  title     = {History of Interactive Theorem Proving},
  booktitle = {Computational Logic},
  series    = {Handbook of the History of Logic},
  volume    = {9},
  pages     = {135--214},
  publisher = {Elsevier},
  year      = {2014},
  note = {\url{https://www.cl.cam.ac.uk/~jrh13/papers/joerg.pdf}},
  XXXurl       = {https://doi.org/10.1016/B978-0-444-51624-4.50004-6},
  XXXdoi       = {10.1016/B978-0-444-51624-4.50004-6},
}

@incollection{kumar-et-al-2014,
  author    = {Ramana Kumar and
               Magnus O. Myreen and
               Michael Norrish and
               Scott Owens},
  editor    = {Suresh Jagannathan and
               Peter Sewell},
  title     = {{CakeML}: A Verified Implementation of {ML}},
  booktitle = {{POPL} 2014},
  pages     = {179--192},
  publisher = {{ACM}},
  year      = {2014},
  note = {\url{https://cakeml.org/popl14.pdf}}
}

@book{knuth-1986,
  author    = {Donald E. Knuth},
  title     = {The \TeX{}book},
  publisher = {Addison-Wesley},
  year      = {1986},
  note = {\url{http://www.ctex.org/documents/shredder/src/texbook.pdf}}
}

@inproceedings{watt-2018,
  author    = {Conrad Watt},
  editor    = {June Andronick and
               Amy P. Felty},
  title     = {Mechanising and Verifying the {WebAssembly} Specification},
  booktitle = {CPP 2018},
  pages     = {53--65},
  publisher = {{ACM}},
  year      = {2018},
  note = {\url{https://www.cl.cam.ac.uk/~caw77/papers/mechanising-and-verifying-the-webassembly-specification.pdf}}
}

@inproceedings{lewis-2019,
  author    = {Robert Y. Lewis},
  editor    = {Assia Mahboubi and
               Magnus O. Myreen},
  title     = {A formal proof of {H}ensel's lemma over the \textit{p}-adic integers},
  booktitle = {{CPP} 2019},
  pages     = {15--26},
  publisher = {{ACM}},
  year      = {2019},
  note = {\url{https://arxiv.org/pdf/1909.11342.pdf}},
  XXXurl       = {https://doi.org/10.1145/3293880.3294089},
  XXXdoi       = {10.1145/3293880.3294089}
}

@inproceedings{gopinathan-sergey-2020,
  author    = {Kiran Gopinathan and
               Ilya Sergey},
  editor    = {Shuvendu K. Lahiri and
               Chao Wang},
  title     = {Certifying Certainty and Uncertainty in Approximate Membership Query
               Structures},
  booktitle = {CAV 2020, Part {II}},
  series    = {Lecture Notes in Computer Science},
  volume    = {12225},
  pages     = {279--303},
  publisher = {Springer},
  year      = {2020},
  note = "\url{https://arxiv.org/abs/2004.13312}"
}

@book{lipovaca-2011,
 author = {Lipovaca, Miran},
 title = {Learn You a {H}askell for Great Good!: A Beginner's Guide},
 year = {2011},
 isbn = {1593272839, 9781593272838},
 edition = {1st},
 publisher = {No Starch Press},
 note = "\url{http://learnyouahaskell.com/}"
}

@inproceedings{baanen-2020,
  author    = {Anne Baanen},
  editor    = {Nicolas Peltier and
               Viorica Sofronie{-}Stokkermans},
  title     = {A {L}ean Tactic for Normalising Ring Expressions with Exponents (Short
               Paper)},
  booktitle = {IJCAR 2020},
  series    = {Lecture Notes in Computer Science},
  volume    = {12167},
  pages     = {21--27},
  publisher = {Springer},
  year      = {2020},
  XXXurl       = {https://doi.org/10.1007/978-3-030-51054-1\_2},
  XXXdoi       = {10.1007/978-3-030-51054-1\_2},
  note = "\url{https://lean-forward.github.io/ring_exp/paper.pdf}"
}

@inproceedings{limperg-2021,
  author    = {Jannis Limperg},
  editor    = {Catalin Hritcu and
               Andrei Popescu},
  title     = {A novice-friendly induction tactic for {Lean}},
  booktitle = {{CPP} '21},
  pages     = {199--211},
  publisher = {{ACM}},
  year      = {2021},
  XXXurl       = {https://doi.org/10.1145/3437992.3439928},
  XXXdoi       = {10.1145/3437992.3439928},
  note = "\url{https://arxiv.org/pdf/2012.08990.pdf}"
}

@mastersthesis{carneiro-2019,
  title = "The Type Theory of {L}ean",
  author = "Mario Carneiro",
  note = "\url{https://github.com/digama0/lean-type-theory/releases/download/v1.0/main.pdf}",
  school = "Carnegie Mellon University",
  type = "{MSc} thesis",
  year = 2019}

@inproceedings{buzzard-et-al-2020,
  author    = {Kevin Buzzard and
               Johan Commelin and
               Patrick Massot},
  editor    = {Jasmin Blanchette and
               Catalin Hritcu},
  title     = {Formalising perfectoid spaces},
  booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
               Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
               20-21, 2020},
  pages     = {299--312},
  publisher = {{ACM}},
  year      = {2020},
  XXXurl       = {https://doi.org/10.1145/3372885.3373830},
  XXXdoi       = {10.1145/3372885.3373830}
}

%%% TODO: Pages
@inproceedings{limperg-from-2023,
  author    = {Jannis Limperg and Asta Halkjær From},
  editor    = {Brigitte Pientka and
               Steve Zdancewic},
  title     = {Aesop: White-Box Best-First Proof Search for {L}ean},
  booktitle = {{CPP} '23},
  XXXpages     = {199--211},
  publisher = {{ACM}},
  year      = {2023},
  XXXurl       = {https://doi.org/10.1145/3437992.3439928},
  XXXdoi       = {10.1145/3437992.3439928},
  note = "\url{https://people.compute.dtu.dk/ahfrom/aesop-camera-ready.pdf}"
}
