Bachelor Thesis

In this project, the student should implement a linter for Isabelle in Isabelle/Scala. A linter is a program that checks the source code for patterns that are undesirable.

Undesirable patterns in Isabelle could be automated proofs that are prone to break after making small changes or more trivial things such as incorrect indentation with respect to some style guide. To this end, our team currently devises a list of guidelines. Some practical examples can also be found in Gerwin Klein's guide on Isabelle proofs.

The linter should provide an interface to define lints, switching lints on and off both globally and locally, and a way to report the lints both in a human and a machine-readable format. The design of the interface can be adapted from linters in other languages such as clippy or pylint.

Remarks:

  1. The student must be familiar with functional programming paradigms as the linter will be written in Isabelle/Scala.
  2. The Isabelle/Scala codebase as well as the PIDE protocol (the protocol used to process Isabelle code) are mostly undocumented. A steep learning curve is thus to be expected in the initial phase of the project.
Programming language:
Scala
Prerequisites:
Familiarity with functional programming; English
Supervisor:
Lukas Stevens
Professor:
Prof. Tobias Nipkow, email {nipkow} AT [in.tum.de]