Séminaire Cambium, Inria Paris
                              Salle Grace Hopper
                           Jeudi 28 novembre, 10h30

                               Benjamin Werner
                                 LIX & Inria

              Actema: a graphical and gestural front-end for Coq

Actema is a graphical user-interface to build formal proofs through
graphical actions. We will present the current prototype which acts as
a front-end to Coq, covering theoretical and practical aspects.

The central paradigm is that many proof-steps can be described as
interactions between two subexpressions, of either the goal to be
proved and of a hypothesis, or two hypotheses. The logical approach
known as "Deep Inference" provides the tools for implementing this
paradigm in a systematic and well-understood way. One main advantage
of a graphical interface over traditional textual commands is that the
user can designate subexpressions in a very quick and intuitive way.
This enables further features which I will try to demonstrate,
including:

- being able to act on propositions independently from its root
  symbol, including under quantifiers,

- a generalization of the search tools (as they are known in Coq),

- dispensing with the need for existential variables, at least in many
  cases,

- the ability to chose graphically where rewriting by propositional
  equalities of computations are to be performed,

- allowing an approach of proof by refinement, be it in forward or
  backward manner.

I will also discuss implementation and architecture issues, as well as
possible future improvements and bottlenecks.

Joint work with PY Strub, K Chaudhuri, P Donato and M Bouverot.

            Vous pouvez vous abonner à nos annonces de séminaires:
                     http://cambium.inria.fr/seminar.html

             Nos séminaires sont accessibles en ligne en direct
                            via le lien ci-dessus.