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.
Student: Yecine Megdiche
Supervisor:
Fabian Huch and Lukas Stevens
Professor:
Prof. Tobias Nipkow, email {nipkow} AT [in.tum.de]