Project Description:
Holbert is a browser-based graphical proof assistant implemented in Haskell whose terms are given in untyped λ-calculus. It is designed to be used as an educational tool. Currently, proofs and definitions (together called a theory) are just dumped as JSON files of the internal data structures of the proof assistant, which poses a number of problems:
- The files cannot be read by a human without loading them first into the proof assistant.
- The files are not readable across different versions of Holbert, and as new features are added, old documents can no longer be read.
This project would be focused on implementing a parser and printer to a text-based file format for Holbert theories. This necessitates the development of a concise, human-readable text based proof format for natural deduction proofs. Inspiration may be taken from related work like SasyLF. The parser may also check proofs as they are parsed using Holbert’s proof kernel, so that invalid proofs are not admitted.
As a stretch goal, the format could be made extensible, and with support for automatic migrations between versions of the file format.
Required Skills:
- Haskell Programming
- Understanding of Logic