Back to University of Twente portal
| 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 |
Description
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).