LFU:online

Understanding of interactive theorem proving; ability to specify programs and proofs in the Isabelle/HOL proof assistant; acquisition of the ability to independently educate themselves in the field.

This course provides knowledge about interactive theorem proving with a focus on the Isabelle proof assistant using higher-order logic (HOL). The following topics will be discussed:

• higher-order logic
• Isabelle's proof language Isar
• natural deduction in Isabelle
• functional programming in Isabelle
• inductive definitions
• code generation
• selection of advanced topics

Lecture; presentation of exercise sheets by students

Continuous assessment based on regular written and oral contributions. There will further be a project work that will be graded at the end of the semester.

See homepage of this course.

Knowledge about logic and functional programming.