Teaching
Next semester, I will co-organise our group's seminar.
Together with Henriette Färber I'm organising a lab course on interactive theorem proving using Isabelle/HOL in the winter 25/26 semester.
Interests
- Formalisation of Mathematics and Logic in interactive theorem provers (such as Isabelle, and sometimes Agda)
- Usable code extraction from formally proven developments
- Category theory
- 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: 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! I list some topics on the group's combined list of offers, but don't take this as exhaustive – feel free to suggest your own ideas.
Publications
| Titel | Autor(en) | Quelle |
|---|---|---|
| Observable Semantics for Characterising Consistency Between Heterogeneous Models | Henriette Färber, Romain Pascual, Terru Stübinger und Mattias Ulbrich | Software Engineering and Formal Methods (SEFM 2025) |
| Titel | Autor(en) | Quelle |
|---|---|---|
| Extending Isabelle/HOL's Code Generator with Support for the Go Programming Language | Terru Stübinger und Lars Hupel | 26th International Symposium on Formal Methods (FM 2024), Teil II |
| Go Code Generation for Isabelle | Terru Stübinger und Lars Hupel | Archive of Formal Proofs |