Chair of Computer Architecture

University Freiburg

Seminar Higher Order Theorem Proving with Isabelle Winter Semester 2022 / 2023

In this Seminar we will discuss case-studies and recent technical developments in the context of high-order theorem proving with focus on the Isabelle prover.

Remark: this seminar will happen in-presence as long as reasonable.

This seminar will be composed of two parts. The first part will be an Isabelle crash course. The aim is to make Isabelle wizards out of you, but to give you a better base to understand the papers. The second part is a seminar where you have to present papers (including some details on the Isabelle formalization).

More details are available on ILIAS.