@article(Avigad2014,
 author       = {Jeremy Avigad and John Harrison},
 year         = {2014},
 title        = {Formally Verified Mathematics},
 journal      = {Communications of the ACM},
 volume       = {57},
 number       = {4},
 pages        = {66–75},
 doi          = {10.1145/2591012},
)
@misc(LeanCourse2022,
 author       = {Jasmin Christian Blanchette},
 year         = {2021},
 title        = {Logical Verification},
 howpublished = {\url{https://lean-forward.github.io/logical-verification/2021/}},
 note         = {Course description.},
)
@misc(NNG2021,
 author       = {Kevin Buzzard and Mohammad Pedramfar},
 year         = {2021},
 title        = {The Natural Number Game, version 1.3.3},
 howpublished = {\url{https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/}},
 note         = {Educational game.},
)
@misc(LeanCourse2015,
 author       = {Edmund M. Clarke and Jeremy Avigad},
 year         = {2015},
 title        = {Interactive Theorem Proving},
 howpublished = {\url{http://leanprover.github.io/cmu-15815-s15/}},
 note         = {Course description.},
)
@inproceedings(LSFA,
 author       = {Asta Halkj{\ae}r From and Frederik Krogsdal Jacobsen and J{\o}rgen Villadsen},
 year         = {2022},
 title        = {{SeCaV}: A Sequent Calculus Verifier in {Isabelle/HOL}},
 editor       = {Ayala-Rincon, Mauricio and Eduardo Bonelli},
 booktitle    = {{\rm Proceedings 16th} Logical and Semantic Frameworks with Applications, {\rm Buenos Aires, Argentina (Online), 23rd - 24th July, 2021}},
 series       = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {357},
 publisher    = {Open Publishing Association},
 pages        = {38--55},
 doi          = {10.4204/EPTCS.357.4},
)
@inproceedings(ThEdu20,
 author       = {Asta Halkj{\ae}r From and J{\o}rgen Villadsen and Patrick Blackburn},
 year         = {2020},
 title        = {Isabelle/{HOL} as a Meta-Language for Teaching Logic},
 editor       = {Pedro Quaresma and Walther Neuper and Jo{\~{a}}o Marcos},
 booktitle    = {Proceedings 9th International Workshop on Theorem Proving Components for Educational Software, {ThEdu@IJCAR} 2020, Paris, France, 29th June 2020},
 series       = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {328},
 publisher    = {Open Publishing Association},
 pages        = {18--34},
 doi          = {10.4204/EPTCS.328.2},
)
@conference(TFPIE,
 author       = {Asta Halkjær From and Jørgen Villadsen},
 year         = {2021},
 title        = {Teaching Automated Reasoning and Formally Verified Functional Programming in {Agda} and {Isabelle/HOL}},
 booktitle    = {10th International Workshop on Trends in Functional Programming in Education ({TFPIE} 2021) --- Presentation Only / Online Papers},
 pages        = {1--20},
 url          = {https://wiki.tfpie.science.ru.nl/TFPIE2021},
)
@inproceedings(Nipkow-LSD,
 author       = {Tobias Nipkow},
 year         = {2012},
 title        = {Teaching Semantics with a Proof Assistant: No More {LSD} Trip Proofs},
 editor       = {Viktor Kuncak and Andrey Rybalchenko},
 booktitle    = {Verification, Model Checking, and Abstract Interpretation - 13th International Conference, {VMCAI} 2012, Philadelphia, PA, USA, January 22-24, 2012. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {7148},
 publisher    = {Springer},
 pages        = {24--38},
 doi          = {10.1007/978-3-642-27940-9\_3},
)
@manual(prog-prove,
 author       = {Tobias Nipkow},
 year         = {2021},
 title        = {Programming and Proving in {Isabelle/HOL} (Tutorial)},
 note         = {\url{https://isabelle.in.tum.de/doc/prog-prove.pdf}},
)
@inproceedings(Nipkow-CPP,
 author       = {Tobias Nipkow},
 year         = {2021},
 title        = {Teaching algorithms and data structures with a proof assistant (invited talk)},
 editor       = {Catalin Hritcu and Andrei Popescu},
 booktitle    = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021},
 publisher    = {{ACM}},
 pages        = {1--3},
 doi          = {10.1145/3437992.3439910},
)
@book(Isabelle02,
 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(Pierce09,
 author       = {Benjamin C. Pierce},
 year         = {2009},
 title        = {Lambda, the Ultimate {TA}: Using a Proof Assistant to Teach Programming Language Foundations},
 booktitle    = {Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming},
 series       = {ICFP '09},
 publisher    = {Association for Computing Machinery},
 address      = {New York, NY, USA},
 pages        = {121–122},
 doi          = {10.1145/1596550.1596552},
)
@book(Pierce:SF1,
 author       = {Benjamin C. Pierce and Arthur Azevedo de Amorim and Chris Casinghino and Marco Gaboardi and Michael Greenberg and Cătălin Hriţcu and Vilhelm Sjöberg and Brent Yorgey},
 year         = {2022},
 title        = {Logical Foundations},
 series       = {Software Foundations},
 volume       = {1},
 publisher    = {Electronic textbook},
 note         = {Version 6.2, \url{http://softwarefoundations.cis.upenn.edu}},
)
@inproceedings(nadea,
 author       = {J{\o}rgen Villadsen and Andreas Halkj{\ae}r From and Anders Schlichtkrull},
 year         = {2018},
 title        = {{Natural Deduction Assistant ({NaDeA})}},
 editor       = {Pedro Quaresma and Walther Neuper},
 booktitle    = {Proceedings 7th International Workshop on Theorem proving components for Educational software, {THedu@FLoC} 2018, Oxford, United Kingdom, 18 July 2018},
 series       = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {290},
 publisher    = {Open Publishing Association},
 pages        = {14--29},
 doi          = {10.4204/EPTCS.290.2},
)
@inproceedings(ThEdu21,
 author       = {J{\o}rgen Villadsen and Asta Halkj{\ae}r From and Patrick Blackburn},
 year         = {2022},
 title        = {Teaching Intuitionistic and Classical Propositional Logic Using {I}sabelle},
 editor       = {Jo{\~ao} Marcos and Walther Neuper and Pedro Quaresma},
 booktitle    = {{\rm Proceedings 10th International Workshop on} Theorem Proving Components for Educational Software, {\rm (Remote) Carnegie Mellon University, Pittsburgh, PA, United States, 11 July 2021}},
 series       = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {354},
 publisher    = {Open Publishing Association},
 pages        = {71--85},
 doi          = {10.4204/EPTCS.354.6},
)
@article(SLAI-HOL,
 author       = {Jørgen Villadsen},
 year         = {2022},
 title        = {A Formulation of Classical Higher-Order Logic in {Isabelle/Pure}},
 journal      = {Journal of Logic and Artificial Intelligence (LAI)},
 note         = {Accepted},
)
@inproceedings(FMTea,
 author       = {Jørgen Villadsen and Frederik Krogsdal Jacobsen},
 year         = {2021},
 title        = {{Using Isabelle in Two Courses on Logic and Automated Reasoning}},
 editor       = {João F. Ferreira and Alexandra Mendes and Claudio Menghi},
 booktitle    = {Formal Methods Teaching},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 pages        = {117--132},
 doi          = {10.1007/978-3-030-91550-6_9},
)
@manual(isar-ref,
 author       = {Makarius Wenzel},
 year         = {2021},
 title        = {The {I}sabelle/{I}sar {R}eference {M}anual},
 note         = {\url{https://isabelle.in.tum.de/doc/isar-ref.pdf}},
)