@inproceedings{DBLP:journals/corr/abs-1712-09288,
  author    = {Robert Y. Lewis},
  editor    = {Catherine Dubois and
               Bruno Woltzenlogel Paleo},
  title     = {An Extensible Ad Hoc Interface between {L}ean and {M}athematica},
  booktitle = {Workshop on Proof eXchange for Theorem Proving {\upshape(}PxTP 2017{\upshape)}},
  series    = {{EPTCS}},
  volume    = {262},
  pages     = {23--37},
  year      = {2017},
  url       = {https://doi.org/10.4204/EPTCS.262.4},
  doi       = {10.4204/EPTCS.262.4},
  timestamp = {Wed, 12 Sep 2018 01:05:13 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1712-09288},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@book{DBLP:books/daglib/0032840,
  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{DBLP:books/daglib/0005958,
  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{LoVe:hindley-1969,
  author = "Hindley, J. Roger",
  year = 1969,
  title = "The Principal Type-Scheme of an Object in Combinatory Logic",
  journal = "Trans. Amer. Math. Soc.",
  number = 146,
  pages = "29--60"}

@article{DBLP:journals/jcss/Milner78,
  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},
  url       = {https://doi.org/10.1016/0022-0000(78)90014-4},
  doi       = {10.1016/0022-0000(78)90014-4},
  timestamp = {Wed, 14 Nov 2018 10:33:58 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/jcss/Milner78},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/sigplan/Perlis82,
  author    = {Alan J. Perlis},
  title     = {Epigrams on Programming},
  journal   = {{SIGPLAN} Notices},
  volume    = {17},
  number    = {9},
  pages     = {7--13},
  year      = {1982},
  url       = {https://doi.org/10.1145/947955.1083808},
  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 Reference Manual: Release 3.3.0",
  author = "Jeremy Avigad and Gabriel Ebner and Sebastian Ullrich",
  note = "\url{https://leanprover.github.io/reference/}",
  year = 2018
}

@book{theorem-proving-in-lean,
  title = "Theorem Proving in Lean: Release 3.4.0",
  author = "Jeremy Avigad and Leonardo de Moura and Soonho Kong",
  note = "\url{https://leanprover.github.io/theorem_proving_in_lean/}",
  year = 2019}

@book{programming-in-lean,
  title = "Programming in Lean",
  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 = "Femke van Raamsdonk",
  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},
  url       = {https://doi.org/10.1145/3110278},
  doi       = {10.1145/3110278}
}

@book{nipkow-klein-2014,
  author    = {Tobias Nipkow and
               Gerwin Klein},
  title     = {Concrete Semantics---With Isabelle/HOL},
  publisher = {Springer},
  year      = {2014},
  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 Odd Order Theorem},
  booktitle = {Interactive Theorem Proving ({ITP} 2013)},
  series    = {Lecture Notes in Computer Science},
  volume    = {7998},
  pages     = {163--179},
  publisher = {Springer},
  year      = {2013},
  url       = {https://doi.org/10.1007/978-3-642-39634-2\_14},
  doi       = {10.1007/978-3-642-39634-2\_14},
}

@article{gonthier-2008,
  title = "Formal Proof---{T}he Four-Color Theorem",
  author = "Georges Gonthier",
  journal = "Notices AMS",
  volume = 55,
  number = 11,
  pages = "1382--1393",
  year = 2008}

@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       = {Available at \url{http://arxiv.org/abs/1501.02155}},
}

@inproceedings{harrison-2003,
  author    = {John Harrison},
  title     = {Formal Verification at {I}ntel},
  booktitle = {Logic in Computer Science (LICS 2003)},
  pages     = {45--54},
  year      = {2003},
  publisher = {{IEEE} Computer Society}
}

@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}
}

@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}
}

@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 = {Operating Systems Design and Implementation ({OSDI} 2016)},
  pages     = {653--669},
  publisher = {{USENIX} Association},
  year      = {2016},
  url       = {https://www.usenix.org/conference/osdi16/technical-sessions/presentation/gu},
}

@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}
}

@inproceedings{lochbihler-2010,
  author    = {Andreas Lochbihler},
  editor    = {Andrew D. Gordon},
  title     = {Verifying a Compiler for {J}ava Threads},
  booktitle = {European Symposium on Programming ({ESOP} 2010)},
  series    = {Lecture Notes in Computer Science},
  volume    = {6012},
  pages     = {427--447},
  publisher = {Springer},
  year      = {2010},
  url       = {https://doi.org/10.1007/978-3-642-11957-6\_23},
  doi       = {10.1007/978-3-642-11957-6\_23},
  timestamp = {Tue, 14 May 2019 10:00:41 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/esop/Lochbihler10},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}