Winter Term 2025/26

Theorem Prover Lab Course

Event Type: Praktikum
Target Group: Master Computer Science
Scope: 3 ECTS
Place: 50.19 (InformatiKOM), Room 104 (Seminarraum 2)
Time: Wednesdays 14:00-15:30, starting 2025-10-29
Communication: #theoremproverlab-2526:kit.edu
Course: T-INFO-114691
Ilias: 2400229
Lecturers:

Prof. Bernhard Beckert
Terru Stübinger
Henriette Färber

Content

The first half of this course will be an introduction to Isabelle/HOL:

  • its logic
  • principles of proving: simplication, recursion, inductive definitions & proofs

(more details to follow)

Topics:

Half of the course will be spent on a project. Topics will be agreed on with the organisers after the first half of the course.