Interactive GUI for Programming-Oriented Proof Assistant

Contact

• Jan Liam Verter
• Tomáš Petříček

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

• SASyLF: An Educational Proof Assistant for Language Theory
• PLT Redex: Domain-specific language for specifying and debugging operational semantics