Teaching
Together with Henriette Färber I will organise a lab course on interactive theorem proving using Isabelle/HOL in the winter 25/26 semester (more information to follow).
Interests
- Formalised Mathematics using interactive theorem provers such as Isabelle
- Usable code extraction from from formally proven developments
- Foundations of Logic
- As part of the Convide Project I work on formalising consistency in model-driven engineering
Open invitation: Inspired by my former supervisor Lars Hupel, I offer an open invitation: if want to talk (or are curious) about any of the above topics, I want to talk to you! Feel free to send me an email, come to my office, or approach me at a conference or workshop.
If you're a student at KIT: I don't currently have a list of project ideas published, but if you're looking for a (Forschungspraktikum, PdF, ...) project or thesis touching on the above topics, feel free to reach out & let's talk about possibilities!
Publications
| Title | Author(s) | Source |
|---|---|---|
| Extending Isabelle/HOL's Code Generator with Support for the Go Programming Language | Terru Stübinger and Lars Hupel | 26th International Symposium on Formal Methods (FM 2024), Part II |
| Go Code Generation for Isabelle | Terru Stübinger and Lars Hupel | Archive of Formal Proofs |