Master’s practical course, Master’s thesis, or IDP

The purpose of this project is to add various missing bits of group theory to HOL-Algebra, with a particular focus on finite groups. Topics of interest include:

Experience with Isabelle/HOL is required. Knowledge of basic group theory is recommended. Experience with locales or even HOL-Algebra itself would be helpful, but is not required.

Manuel Eberl, email {eberlm} AT []

Prof. Tobias Nipkow, Raum MI 00.09.055, email {nipkow} AT []