Master’s Thesis, Bachelor’s Thesis, or Practical Course

Many times in formal verification, we set definitions and prove theorems about particular structures, only to discover later that our results should be applicable to similar, though definitionally different, structures. As an example, if we define addition on integers Z and prove it to be commutative, we would like to obtain an analogous operation on natural numbers N and its commutativity proof for free.

In Isabelle/HOL, the Lifting and Transfer package offers such automation for a limited fragment of structural equivalences (e.g. subtypes and quotients). Very recently, these equivalences have been generalised to a broader class by this project’s advisor. The paper draft can be found here.

The aim of the project is to create automation support for this new class of equivalences in Isabelle/HOL. This requires both formalisation and functional programming skills. Acquaintance with Isabelle/ML is a plus.

Prerequisites: Experience with Isabelle and functional programming experience.

Advisor: Kevin Kappelmann

Supervisor: Prof. Tobias Nipkow