A connecting theme of my research is the design of a logical framework that
- encompasses set/model and type/proof theoretical frameworks and different mathematical foundations without committing to any of them,
- leverages modularity on all levels,
- supports the integration of reasoning and computation systems based on different logics,
- is seamlessly integrated with tools such as compilers, IDEs, databases, browsers,
- scales to the web.
Major research projects I am/was involved in are
- the OpenDreamKit project on digital research environments for mathematics (EU, 2015-2019)
- the OAF project on integrating formal libraries (DFG, 2014-2020)
- the LATIN project on formalizing logics and logic translations (DFG, 2009-2012) abstract)
Check out this picture of me in front of the LATIN graph (taken at LRI in Paris).
- the MMT language and system, a foundation-independent representation language for formal knowledge
Check out the video of my talk on MMT in Andrej Bauer's seminar on Every Proof Assistant
- the Twelf module system, a module system for Twelf
Current work, preprints, and paper drafts (always outdated)
All new/recent papers are available in the publications section below.
Publications (often outdated)
All list, tables, and bibtex files are automatically generated using my Scala package for bibliographies. Contact me if you want to use it as well or if you spot any errors.
If I make the slides of one of my talks available, they are linked from the corresponding paper in the publication lists above.
I use this set of slides when I give overview talks of my research.
I have received my habilitation at Jacobs University in 2014. My topic was
A Scalable Logical Framework.
My habilitation committee consisted of the following Jacobs University professors:
I have received my PhD at Jacobs University in 2008. My thesis topic was
Representing Logics and Logic Translations.
My supervisor was
and my further thesis advisors were
Curriculum Vitae (often outdated)
You can find my extended CV here.