|title:||Prove your (functional) Algorithm in Isabelle/HOL|
|keywords:||interactive theorem provers, program correctness|
|topics:||Algorithms and Data Structures , Logics and semantics|
|committee:||dr. Peter Lammich|
Interactive Theorem Provers (ITPs) provide a way to develop computer checked (mathematical) proofs. In particular, they can be used to prove programs correct. In this project, you will learn to use an ITP, and apply it to prove correct a functional program or data structure of your choice (agreed on with the supervisor).