1-2 PhD Positions in the OAF Project

The Open Archive of Formalizations will provide an open infrastructure to translate and share formalized mathematical knowledge such as theories, definitions, and proofs between mutually incompatible foundations (e.g., set theory, higher-order logic, constructive type theory, etc.), library formats, and library structures. The OAF system will be based on a uniform foundation-independent representation format for libraries, which allows formalizing the logical foundations alongside the libraries and thus acts as framework for aligning libraries.

Several Positions in the OpenDreamKit Project

The Open Digital Research Environment Toolkit for the Advancement of Mathematics (OpenDreamKit) will deliver a flexible toolkit enabling research groups to set up Virtual Research Environments, customised to meet the varied needs of research projects in pure mathematics and applications, and supporting the full research life-cycle from exploration, through proof and publication, to archival and sharing of data and code, including popular tools such as LinBox, MPIR, Sage(sagemath.org), GAP, PariGP, LMFDB, and Singular.

Within OpenDreamKit, our group will in particular develop a unified framework for mathematical data and computation and apply it to the integration of mathematical libraries and programming environments.
We are generally flexible to develop PhD topics together with strong candidates.
Some example PhD topics that could be assigned within these positions are given below.

Our Group

Jacobs University Bremen is a private, English-speaking research university in Germany.
The KWARC group conducts research on the representation and management of formal and informal knowledge in the STEM disciplines (Science, Technology, Engineering, and Mathematics).

Our interests cover the whole range from formal to informal knowledge and include

We build systems that cover these diverse areas uniformly and integrate across domains, languagues, and tools, always combinng logical correctness, wide-range applicability, and large-scale inter-operability.

Application Procedure

Interested candidates can introduce themselves or ask for further information by email to Prof. Michael Kohlhase (m.kohlhaseATjacobs-university.de).
Applications (including the usual documents) should be directed to the same email address.