A language for proofs through actions

Location : LIX, Ecole polytechnique

supervised by : Benjamin Werner and Pierre-Yves Strub

The aim of the project actema (active mathematics) is the construction of a novel interface for constructing formal proofs. In this paradigm,
proofs steps are not anymore described by written commands (proofs tactics) but through actions performed in a graphical user interface. For instance:

•  clicks or double-clicks on specific subterms of either hypotheses or proof-goals,
• drag-and-drop of a hypothesis on a goal, or a specific subterm of a goal.

Some very simple possible behaviors of mathematical objects include:

• Double-click on a goal of the form A/\B transforms it into two goals A and B.
• Double-click on the left (resp. right) part of a goal A\/B transforms it into a goal A (resp. B).
• Dragging a hypothesis A->B to a goal B will transform it into a goal A. Dragging a hypothesis "forall x, A(x) -> B(x)" to a goal A(t) will transform it into a goal B(t).

One can imagine various versions depending upon the level of the intended users; for instance, advanced users could have access to more sophisticated behaviors than undergraduate students.

To a certain extent, this effort can be described as a continuation of the proof-by-pointing concept which was invented and developed in the nineties by the team of Gilles Kahn. Differences are:

• The means of recent interfaces' interactions (drag-and-drop, tactile screens, multi-touch) which allow a richer interaction and a more streamlined graphical layout.
• The modern software libraries for interfaces make the development and the maintenance of such a software much easier.

A first prototype is currently developed and tested at LIX. The front-end, or interface, runs in a standard html/javascript environment. The back-end of the system is a little prover implemented in OCaml. The link between front and back end is facilitated by using the JSofOcaml translator.

Although one can imagine fitting such an interface as a front-end on an existing proof system like Coq of HOL, the current aim is to experiment, to validate the idea, and mainly determine a set of behaviors. That is how various mathematical objects should react to user actions.

The topic of the internship is define a language to describe these actions. This should be at the same time understandable and high-level, and, on the other hand, sufficiently close to the implementation in order to quickly test suggested new behaviors.

The internship is thus at the intersection of many kind of interests and skills : formal proofs and logic, languages, user interfaces, automated deduction and programming. It could lead to a PhD subject.


References : Proof by pointing. Yves Bertot, Gilles Kahn and Laurent Thery. TACS 94, Sendai, LNCS 789, Springer-Verlag, 1994.