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.

• A Universal Framework for Computation
  Our frameworks and infrastructure are already very strong for declarative, logical, and informal/narrative content, but lack deep support for computational content such as programming languages, algorithms, and libraries.
  Within this PhD thesis, we hope extend our OMDoc/MMT framework toward computational content. This would in particular include case studies in the OpenDreamKit project (e.g., programming languages like Scala or Python, computer algebra systems like SageMath or GAP, and their libraries).
• Integrating Libraries and Databases of Mathematical Knowledge
  Recently computational mathematicians have built more and more libraries of mathematical objects and models.
  Examples are the Online Encyclopedia of Integer Sequences (OEIS), the FindStat library of combinatorial objects, the Library of L-Functions and Modular Forms (LMFDB), or the Math Geneology Project.
  In this PhD thesis, we want to extend our OMDoc/MMT framework with primitives for representing such libraries uniformly as theory graphs and extend our knowledge management algorithms to cope with these large data volumes.

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

• logics and foundations of mathematics
• formalizing/verifying knowledge
• informal and semi-formal documents (specifications, papers, web pages, etc.)
• domain-specific applications (spreadsheets, CAD, etc.)
• knowledge management (search, user interfaces, system integration, etc.)

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.