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