Bachelor Thesis
With the emergence of the language server protocol (LSP) [1], integrating new languages and frameworks into existing modern IDEs has become a feasible task. For the interactive theorem prover Isabelle, a Visual Studio code (VScode) plugin has already been introduced [2], which is makes it possible to develop formal theories in a more common IDE than the highly adapted Isabelle/jEdit.
However, Issues with mathematical symbols, slow highlighting for large theory files, partially missing markup make this plugin difficult to use. Moreover, many semantic IDE features are absent.
The task of this thesis is to rework the Isabelle/VScode integration in order to provide first-level support of Isabelle symbols and markup, as well as adding support for important Prover IDE functionality. While the backend Isabelle functionality is built in Scala, the frontend functionality of VSCode is based on web technologies.
Your implementation will also be valuable for further developments of Isabelle/jEdit, since future plans involve migrating that frontend to a web-based stack as well.
Prerequisites
Typescript/Web Development Experience; Scala (or similar functional programming language); English
Advisor
Fabian Huch, email {huch} AT [in.tum.de]
Supervisor
Prof. Tobias Nipkow, email {nipkow} AT [in.tum.de]
References
[2] Wenzel, Makarius. “Isabelle/PIDE after 10 years of development.” UITP workshop: User Interfaces for Theorem Provers. 2018.
Results
Students
Denis Paluca Thomas Lindae