Teaching Algorithms and Data Structures with a Proof Assistant

Teaching Algorithms and Data Structures with a Proof Assistant (Invited Talk)

Tobias Nipkow

We report on a new course "Verified Functional Data Structures and Algorithms" taught at the Technical University of Munich. The course first introduces students to interactive theorem proving with the Isabelle proof assistant. Then it covers a range of standard data structures, in particular search trees and priority queues: it is shown how to express these data structures functionally and how to reason about their cor- rectness and running time in Isabelle.

pdf ACM/CPP21

BibTeX:

@inproceedings{Nipkow-CPP21,
author={Tobias Nipkow},
title={Teaching Algorithms and Data Structures with a Proof Assistant (Invited Talk)},
booktitle={Certified Programs and Proofs, {CPP} 2021},
editor={C. Hritcu and A. Popescu},
publisher={ACM},year=2021}