Overview
| Module | Bachelor-Praktikum (Practical Course for BSc students), IN0012 Master-Praktikum (Practical Course for MSc students, IN2106 |
| Prerequisites | Basic knowledge of Isabelle (e.g. through ‘Functional Data Structures’, IN2347, ‘Semantics’, IN2055) |
| Language | German, English |
| Organisation | Prof. Tobias Nipkow |
Content
During the practical course students will work (guided by an advisior) on a practical problem involving the interactive theorem prover/proof assistant Isabelle. Most topics will involve using Isabelle to formalize some material, but there will also be some topics offered allowing for work on Isabelle itself and related tools. The goal of this course is providing an oppurtunity to experience actual, practical work involving proof assistants, not contrived examples from a classroom setting. Therefore previous experience with Isabelle is mandatory.
Course structure
The practical course will run throughout the lecture period of the summer semester 2025. If needed (exchange semesters, work, exams, …) we can accomodate students starting early or working on their project also during the lecture free period of SS25. Students will (independently or in small groups) work on their projects guided by an advisior. There are no fixed, regular meetings of the entire course, however students are encouraged to regularly meet with their advisors. The grading will be based on the work perfomed, there will not be any graded exams or presentations.
Preliminary meeting
None
Application
If you want to participate in the practical course, please send an email to Prof. Nipkow until 19.2.25. In it, please list your prior experience with Isabelle.