Tobias Heindel (Heliax GmbH) (May 18 2024 at 06:19): Tobias Heindel (Heliax GmbH) (May 18 2024 at 06:19):This page on course material at TUM deserves some care (broken links), and the following course material, taken from here, might be a good addition.
Filip Maric (University of Belgrade): Experiences in teaching an introductory interactive theorem proving course to computer science undergraduates
Abstract: For several years we have been offering an elective course "Introduction to Interactive Theorem Proving" to our computer science undergraduates. Although the course has extensive mathematical content and is not directly applicable to jobs in the IT industry, it is very popular with students. The course is based on the proof assistant Isabelle/ HOL and is divided into two parts: (1) proofs, proof languages and formalisation of mathematics and (2) functional programming and verification of algorithms and data structures. We keep the pace slow and introduce new concepts very gently, but in the end students still manage to do a project in which they formalise an IMO problem or verify a simple algorithm or data structure. In this PAT course I will give a short introduction to Isabelle/ HOL using the same didactic approach and exercises that our students use. I will also talk about our experiences in class.
Slides: slides-pat2023-maric.pdf
Examples: FilipMaricPAT2023.zip
EDIT: I just found this ongoing course http://cl-informatik.uibk.ac.at/teaching/ss24/itpIsa/content.php?lan=en
Kevin Kappelmann (May 18 2024 at 07:04):Hi Tobias, the linked page is obsolete. The new page is here :
https://isabelle.systems/courses.html
You can update the entries by creating a pull request
https://github.com/isabelle-prover/isabelle-prover.github.io
Last updated: Dec 21 2024 at 12:33 UTC