[Agda] PhD and Postdoc Positions - KWARC, Jacobs University Bremen

[Michael Kohlhase]

The KWARC group [1] at Jacobs University Bremen [2] is looking for
Ph.D. candidates and PostDocs in multiple projects, e.g. [3,4].

See also
http://www.jacobs-university.de/jobs/phd-and-postdoc-positions-kwarc-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.

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

------------------------------

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.

1) 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).

2) 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.

3) Knowledge Management for Cognitive Enigineering

Designing technical artifacts such as robots, cranes, or pens is a
knowledge-based, document-centered process (see DIN 6221).
In this PhD thesis, we want to apply formal and informal knowledge
management (theory-graph) methods and active document technologies to
the engineering process and the background knowledge. We want to build
semantic sextensions to CAD systems and Office suites via our semantic
alliance framework to allow Engineers to access the knowledge management
solutions from their usual working environment.

------------------------------

[1] http://kwarc.info

[2] http://www.jacobs-university.de

[3] https://kwarc.info/projects/OAF
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.

[4] http://opendreamkit.org/
The Open Digital Research Environment Toolkit for the Advancement of
Mathematics 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.
   

-- 
----------------------------------------------------------------------
 Prof. Dr. Michael Kohlhase,        Office: Research 1, Room 168
 Professor of Computer Science  Campus Ring 1, 
 Jacobs University Bremen           D-28759 Bremen, Germany
 tel/fax: +49 421 200-3140/-493140  skype: m.kohlhase   
 m.kohlhase at jacobs-university.de http://kwarc.info/kohlhase 
----------------------------------------------------------------------

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151021/4222e716/attachment.html