Bachelor’s/Master’s thesis
The aim is to verify a library of algorithms for listing combinatorial objects: permutations, subsets, partitions, trees, … . There is a rich literature on the subject (see below). Part of the challenge is to find elegant functional programs instead of the universally imperative algorithms given in the literature (Nijenhuis and Wilf even give Fortran programs!). You can find a first Isabelle example here
[1] Knuth, The Art of Computer Programming, Volume 4A, Combinatorial Algorithms
[2] Nijenhuis and Wilf. Combinatorial Algorithms
[3] Stanton and White. Constructive Combinatorics
Prerequisites: Some familiarity with Isabelle/HOL.
Supervisor: Prof. Tobias Nipkow, Raum MI 00.09.055, email {nipkow} AT [in.tum.de]