@inproceedings(IsaFoL,
 author       = {Jasmin Christian Blanchette},
 year         = {2019},
 title        = {Formalizing the Metatheory of Logical Calculi and Automatic Provers in {Isabelle/HOL} (Invited Talk)},
 booktitle    = {Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP)},
 pages        = {1--13},
 doi          = {10.1145/3293880.3294087},
)
@unpublished(EWD:EWD1062,
 author       = {Edsger W. Dijkstra},
 year         = {1989},
 title        = {On an exercise of {T}ony {H}oare's},
 note         = {Circulated privately, \url{http://www.cs.utexas.edu/users/EWD/ewd10xx/EWD1062.PDF}},
)
@book(harrison+09,
 author       = {John Harrison},
 year         = {2009},
 title        = {Handbook of Practical Logic and Automated Reasoning},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9780511576430},
)
@article(jensen2018,
 author       = {Alexander Birch Jensen and John Bruntse Larsen and Anders Schlichtkrull and J{\o}rgen Villadsen},
 year         = {2018},
 title        = {Programming and verifying a declarative first-order prover in {Isabelle/HOL}},
 journal      = {{AI} Communications},
 volume       = {31},
 number       = {3},
 pages        = {281--299},
 doi          = {10.3233/AIC-180764},
)
@article(lamport,
 author       = {Leslie Lamport},
 year         = {1993},
 title        = {How to write a proof},
 journal      = {Global Analysis in Modern Mathematics},
 pages        = {311--321},
 note         = {Also published in \emph{American Mathematical Monthly}, 102(7):600-608, August-September 1995},
)
@article(lamport2,
 author       = {Leslie Lamport},
 year         = {2012},
 title        = {How to write a 21st century proof},
 journal      = {Journal of fixed point theory and applications},
 volume       = {11},
 number       = {1},
 pages        = {43--63},
 doi          = {10.1007/s11784-012-0071-6},
)
@book(nipkow+02,
 author       = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
 year         = {2002},
 title        = {Isabelle/HOL - {A} Proof Assistant for Higher-Order Logic},
 series       = {Lecture Notes in Computer Science},
 volume       = {2283},
 publisher    = {Springer},
 doi          = {10.1007/3-540-45949-9},
)
@inproceedings(DBLP:journals/corr/abs-1803-01473,
 author       = {J{\o}rgen Villadsen and Andreas Halkj{\ae}r From and Anders Schlichtkrull},
 year         = {2017},
 title        = {Natural Deduction and the {I}sabelle Proof Assistant},
 editor       = {Pedro Quaresma and Walther Neuper},
 booktitle    = {Proceedings 6th International Workshop on Theorem proving components for Educational Software (ThEdu)},
 series       = {{EPTCS}},
 volume       = {267},
 pages        = {140--155},
 doi          = {10.4204/EPTCS.267.9},
)
@inproceedings(VilladsenEtAl:PAAR2018,
 author       = {Jørgen Villadsen and Anders Schlichtkrull and Andreas Halkjær From},
 year         = {2018},
 title        = {A Verified Simple Prover for First-Order Logic},
 editor       = {Boris Konev and Josef Urban and Philipp Rümmer},
 booktitle    = {6th Workshop on Practical Aspects of Automated Reasoning (PAAR)},
 series       = {CEUR Workshop Proceedings},
 volume       = {2162},
 address      = {Aachen},
 pages        = {88--104},
 url          = {http://ceur-ws.org/Vol-2162/#paper-08},
)