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 | Simon Roßkopf, Prof. Tobias Nipkow Contact Simon Roßkopf for all course matters, or your advisor (once you have been assigned one). |
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 2024. If needed (exchange semesters, work, exams, …) we can accomodate students starting early or working on their project also during the lecture free period of SS24. 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
There will be an (informal, non-mandatory) kickoff meeting in (probably) 00.09.038 at 14:00 on Monday 05.02.24. The purpose of this meeting is to answer any questions you might have prior to the course.
Application
If you want to participate in the practical course, please send an email to Simon Roßkopf (before the start of the matching). In it, please list your prior experience with Isabelle. A formal letter of application or similar (beyond the mentionend email) is not necessary.