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:
- Decomposition of a group into an interior direct product
- Indexed direct products
- The fundamental theorem of finite(ly generated) abelian groups
- Finite simple groups
Prerequisites:
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.
Advisor:
Manuel Eberl, email {eberlm} AT [in.tum.de]
Supervisor:
Prof. Tobias Nipkow, Raum MI 00.09.055, email {nipkow} AT [in.tum.de]