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).