Interests

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.

Current projects

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)

Slides on DHOL (dependently typed higher-order logic) from my invited talk at the Formalization of Mathematics workshop at the Hausdorff Institute
Slides on the Future of Formalized Mathematics from my talk at the Hausdorff Center
Slides on Exporting Proof Assistant Libraries from my invited talk at the 2022 EuroProofNet WG 4 meeting
Slides on Representing Scientific Knowledge from my invited talk at the 2022 TiPES meeting
Model Theory and Subtyping for Dependently-Typed Higher-Order Logic
Modular Formalization of Formal Systems, i.e., the LATIN2 project
System Description: MMT - A Foundation-Indepedent Logical Framework
Theory Expressions

All new/recent papers are available in the publications section below.

Publications (often outdated)

Chronologically (including all the grey literature)
CV style (grouped by strictness of refereeing)
Coauthors (important publications grouped by coauthor)

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.

Slides

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.

Students

My list of students and their theses

Habilitation

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:

PhD

I have received my PhD at Jacobs University in 2008. My thesis topic was Representing Logics and Logic Translations. My supervisor was Michael Kohlhase, and my further thesis advisors were Herbert Jaeger, Till Mossakowski, and Frank Pfenning.

Curriculum Vitae (often outdated)

You can find my extended CV here.