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