Bachelor’s Thesis, Master’s Thesis
The goal of this project is to formalize a decision procedure for bounded lattices [1]. A bounded lattices is an algebraic structure that has join (\(\sqcup\)) and meet (\(\sqcap\)) operations as well as bottom (\(\bot\)) and top elements (\(\top\)). An example for a bounded lattice would be sets with union as join, intersection as meet, the empty set as bottom and the set of all elements as top. The paper also extends the procedure to support monotone functions over those lattices.
In the project, we will employ Isabelle/HOL to formalise an abstract version of the algorithm to prove its correctness. Depending on the kind of project and whether time permits, the algorithm should also support monotone functions and produce certificates that can be replayed through Isabelle’s inference kernel.
[1] https://link.springer.com/chapter/10.1007/11964810_15. Available here.
Prerequisites: Experience with Isabelle/HOL
Advisor: Lukas Stevens
Professor: Prof. Tobias Nipkow