Jugend forscht: Hilbert meets Isabelle

A group of smart students from Bremen have been working on a formalization of Hilbert’s 10th Problem (DPRM Theorem) in Isabelle since October 2017. See also the forthcoming presentation on the Isabelle Workshop 2018 (13-Jul-2018, Oxford, UK) with the following pre-print paper.

A subgroup of particularly young students have also submitted their contribution to the project in the German science competition “Jugend forscht”, and have now won various prizes, notably the “Prize for Extraordinary Work” by Federal President of Germany, Frank-Walter Steinmeier. The catalog of winners lists the project on page 4, with the following laudatio:

Die Jury war begeistert von der Tiefe und begrifflichen Präzision, mit der sich die drei Jungforscher dem komplexen Thema des formalen Verifizierens annahmen. Formale Verifikation ist ein hochaktuelles und wichtiges Thema. Die anspruchsvolle und außergewöhnliche Forschungsarbeit leistet einen wichtigen Beitrag, die Fundamente der Mathematik noch ein Stück stabiler zu machen.

The jury was enthusiastic about the depth and conceptual precision with which the three young researchers addressed the complex topic of formal verification. Formal verification is a highly topical and important topic. The demanding and extraordinary research work makes an important contribution to making the foundations of mathematics even more stable.
(Translated with www.DeepL.com/Translator)

There are some sources and presentation materials on GitLab.

The Isabelle community is looking forward to the final completion of the formalization!

Isabelle/jEdit as formal IDE

This is my contribution to the F-IDE workshop (14-Jul-2018, Oxford, UK): Isabelle/jEdit as IDE for domain-specific formal languages and informal text documents.

Abstract:

Isabelle/jEdit is the main application of the Prover IDE (PIDE) framework and the default user-interface of Isabelle, but it is not limited to theorem proving. This paper explores possibilities to use it as a general IDE for formal languages that are defined in user-space, and embedded into informal text documents. It covers overall document structure with auxiliary files and document antiquotations, formal text delimiters and markers for interpretation (via control symbols). The ultimate question behind this: How far can we stretch a plain text editor like jEdit in order to support semantic text processing, with support by the underlying PIDE framework?