Reference. Gentzen: A Beginner's Proof Assistant based on Higher Order Logic [oconnor-ugproject-2012]

Existing proof assistants such as Isabelle or Coq are geared towards large-scale, complicated verification projects, and are not ideal educational tools for topics of a fairly formal nature, such as the theoretical foundations of programming languages. In particular, they opt for a proof language that resembles a programming language, rather than the structure typically seen in pen-and-paper proofs. Gentzen is a simple theorem prover we are developing in Haskell, which will be tightly integrated with its user interface, using a structural editor for graphically presented proofs. This allows proof scripts to resemble pen-and-paper proofs, and assists students to focus on the proof, rather than the proof assistant. This report outlines the current state of Gentzen development, and gives a formal treatment of its proof checker semantics.