Progress report for Jacobsuni-FAU
M.Kohlhase
Reporting period from March 2017 to June 2018
Finance and administration
On 18/01/2018 the Jacobs University has officially terminated from the OpenDreamKit project. With the recent grant agreement amendment all responsibilities have gone to FAU; the termination report still needs to be completed.
Finance and admin for the KWARC group (Kohlhase/Rabe) in good hands at FAU now.
There is still an issue about the un-used pre-payment for JacU that needs to be resolved via the coordinator. The agreement is that this should go to FAU in its entirety (modulo possibly some travel funds for Florian Rabe that could go to LRI with his shared appointment).
Hiring
We have hired three researchers on half-positions:
- M. Sc. Tom Wiesing on September 1. 2017 for work on virtual theories and the MathHub.info system
- M. Sc. Theresa Pollinger October 1. 2017 - May 15. 2018 for work on the MitM ongology and interfacing mathematical modelling and simulation systems.
- PD Dr. Florian Rabe (shared appointment with LRI) for foundational work on the MMT system and MitM-based system integration.
This brings FAU to nominal strength after the move.
Achievements
- First working Math-in-the-Middle (MitM)-based distributed computation between GAP, MMT, Singular, and Sage.
- Five major releases of the MMT system (three minor); established a six-week release cycle.
- much improved support for the MitM Foundation, a representation framework for mathematical knowledge featuring subtyping, dependent function and record types, types of models for theories.
- Started the MitM Ontology (a concrete language for mathematics based on the above foundation) with knowledge on elliptic curves, computational group theory, partial differential equations, physical constants, laws, and units formalized in the MitM foundation (collaborations with St. Andrews and WIAS Berlin).
- Surveyed mathematically relevant concrete data types and systematically integrated them into the MMT codec infrastructure
- Progress towards generating API theory graphs for GAP (with St. Andrews), Sage (LRI), LMFDB (Warwick), and Singular (Kaiserslautern).
- Started Jupyter Kernel for MMT
- Four international conference publications and one Journal Article
-
Two M.Sc. Theses: Theresa Pollinger and Tom Wiesing
Work in progress
- Using Jupyter for document-embedded computing; integrating Jupyter widgets.
- Completely reworking MathHub.info based on a React.JS front-end and docker swarm for components (sources at GitHub) after another machine getting hacked via the Drupal front-end.
- API theory graph for PARI/GP
- Inductive types in the MitM Foundation
- scaling MMT Virtual Theories to the LMFDB
- Formalizing of Tannakian Symbols and supporting virtual theories in MathHub (external collaboration with Andreas Holstrom).
- organizing OpenDreamKit Workshops at ICMS (South Bend) and CICM (Hagenberg)
- organizing an OpenMath Workshop at CICM (Hagenberg)
- JSON binding for OpenMath (to make the SCSCP communication with GAP easier).
Workshops and dissemination activities
- OpenMath Workshop at CICM 2017