- Contact

Proof Assistants are often used in programming language research to formalize and prove properties of models of programming languages. Those are typically text-based and have only limited interactive capabilities.

The goal of the project is to design an implement interactive graphical user interface for a theorem prover. The GUI should be able to display proofs about programs in a readable way, use the capabilities of the underlying theorem prover to suggest possible steps in proofs (based on the current proof context) and let user easily correct automatically generated parts of proof.

**References**