Supervisor

Suitable for

Abstract

What?

For many years the generic proof-editor Jape has been providing a "proof by pointing" graphical user interface to support the human-directed discovery of proofs and derivations in a logic defined as a system of inference rules.  The goal of this project is not to reinvent Jape, but to give it a modern semantic substrate, using Lean4: the most recent implementation of a very widely accepted programming language cum proof assistant (See https://lean-lang.org/).

The first substantive piece of work will be come up with a proof of concept implementation of proof-by-pointing in the Jape style for one, perhaps two, straightforward logics. I favour (but don't wish to be dogmatic about) a single-conclusion-sequent presentation of a first-order logic, for example, the logic used in Introduction to Formal Proof.  I also favour (but don't wish to be dogmatic about) using Scala as the language in which to program the front-end.^[1]

Why?

Jape was ahead of its time in several respects:

• Proof by pointing rather than scripting
• Explicit proof-derivation objects evolving (interactive) step-by-step
• Structural views of proof derivations: Fitch-boxed or as inference trees: not just as linear text
• A focus on pedagogy through human interaction, not just the correctness of derivations.

 

At the time Richard Bornat and I designed it Jape was revolutionary in the way it provided straightforward user-directed construction of proofs, as well as supporting a straightforward "logician oriented"  metalanguage for defining inference systems. There are few constraints on the kinds of "logic" with which Jape can cope: our goal was always  to make it possible for someone who isn’t expert in Jape to construct a Jape inference system capable of capturing their logic, proof system, operational semantics, or what-have-you  more or less directly from its presentation in a textbook or paper; then for others to construct derivations in the system  interactively.

Our motivation, and the  principles behind Jape's end-user interfaces, were eventually articulated in a couple of papers delivered at the "User Interfaces for Theorem Provers" conference series that it had catalysed: User Interfaces for Generic Proof Assistants Part I: Interpreting Gestures, and User Interfaces for Generic Proof Assistants Part II: Displaying Proofs and in the (shorter) Formal Aspects of Computing Paper: A Minimal Graphical User Interface for the Jape Proof Calculator. These and others that may be of interest are still readable in the directory https://www.cs.ox.ac.uk/people/bernard.sufrin/jape.org.uk/DOCUMENTS/CURRENT/.

When Jape was born, and for very many years afterwards, nearly all of the work in user interfaces for proof tools addressed the problem(s) of attaching a user interface to a powerful pre-existing proof assistant/theorem prover. Our experience of teaching people to conduct proofs (and other derivations) led us to reject this approach.

 

Jape’s semantic substrate was defined by a carefully constructed inference engine; but at the time of its design we were uninterested in foundational aspects of that engine. The advent of Lean4 has given fresh impetus to the idea of re-embodying the UI principles of Jape in a new logical setting. 

 

 

Note

Subsequent projects ought to be able to take this proof of concept in the direction of other logics (Modal logics, Program logics, Separation logic, etc) and systems formalisable as inference systems. The research challenges there include finding straightforward ways for the "interaction designer" to describe correspondences between user-gestures and the inference rules / tactics to which they should be bound.^[2]

 

^[1] I developed the Glyph User Interface Toolkit (github.com/sufrin/Glyph) for purposes such as this.

^[2] The Jape tactic language had binding constructs to facilitate this; but its rebarbative syntax and ad-hoc semantics meant that Bornat and Sufrin were almost the only people who could use it.