The Coq mailing list

[Christoph Lueth <cxl AT informatik.uni-bremen.de>]

[Apologies if you receive multiple copies.]

          User Interfaces for Theorem Provers, UITP 2005

                A Satellite Workshop of ETAPS 2005
          Edinburgh (Scotland),  Saturday 9th April 2005

                  http://uitp05.inf.ed.ac.uk/

The User Interfaces for Theorem Provers workshop series brings
together researchers interested in designing, developing and
evaluating interfaces for interactive proof systems, such as theorem
provers, formal method tools, and other tools manipulating and
presenting mathematical formulas.

While the reasoning capabilities of interactive proof systems have
increased dramatically over the last years, the system interfaces have
often not enjoyed the same attention as the proof engines themselves.
In many cases, interfaces remain relatively basic and under-designed.
Initial studies by HCI (Human-Computer Interaction) practitioners and
theorem-prover developers working in collaboration have had promising
early results, but much remains to be investigated.

The User Interfaces for Theorem Provers workshop series provides a
forum for researchers interested in improving human interaction with
proof systems.  We welcome participation and contributions from the
theorem proving, formal methods and tools, and HCI communities, both
to report on experience with existing systems, and to discuss new
directions.

UITP 2005 is a one-day workshop to be held on Saturday 9th
April 2005 in Edinburgh, Scotland, as a satellite workshop of ETAPS
2005. Registration, travel and accommodation details can be found on
the ETAPS main website at http://www.etaps05.inf.ed.ac.uk.


Programme
~~~~~~~~~

The following papers have been accepted for the workshop:

* Graham Steel:
  Visualizing First-Order Proof Search

* Martin Homik and Andreas Meier:
  Designing a Proof GUI for Non-Experts: Evaluation of an HCI
  Experiment.

* Dominik Haneberg:
  The User Interface of the KIV Verifcation System: A System Description

* Daniel Winterstein, David Aspinall and Christoph Lüth:
  Proof General / Eclipse: A Generic Interface for Interactive Proof

* Mark Buckley and Christoph Benzmüller:
  System Description: A Dialogue Manager supporting Natural Language
  Tutorial Dialogue on Proofs

* Serge Autexier, Christoph Benzmüller, Armin Fiedler and Henri Lesourd:
  Integrating Proof Assistants as Reasoning and Verification Tools
  into a Scientific WYSIWIG Editor.

* Andrew Cook and Andrew Ireland:
  Proof Animation

* Lucas Dixon:
  Interactive Hierarchical Tracing of Techniques in IsaPlanner

* Catarina Coquand, Dan Synek and Makoto Takeyama:
  An Emacs-interface for Type-based Support for Writing Proofs
  and Programs

* Ewen Denney and Bernd Fischer:
  A Program Certification Assistant Based on Fully Automated
  Theorem Provers

* David Aspinall, Christoph Lüth and Daniel Winterstein:
  Parsing, Editing, Proving: The PGIP Display Protocol

* Jacques Fleuriot and Sean Wilson:
  Combining Dynamic Geometry, Automated Geometry Theorem Proving and
  Diagrammatic Proofs


Authors are encouraged to bring along versions of their systems
suitable for informal demonstration during breaks in the programme of
talks. A final version of the programme will appear on the workshop
website soon.

After the workshop, there will be the opportunity to submit extended
and revised papers to a dedicated volume in the Elsevier Electronic
Notes in Theoretical Computer Science.


Programme Committee
~~~~~~~~~~~~~~~~~~~

  David Aspinall   (Edinburgh, UK, organiser)
  Christoph Lüth   (Bremen, Germany, organiser)
  Yves Bertot      (Sophia, France)
  Richard Bornat   (Middlesex, UK)
  Paul Cairns      (London, UK)
  Erica Melis      (Saarbrücken, Germany)
  Burkhart Wolff   (Zürich, Switzerland)

Attachment: call.pdf
Description: Adobe PDF document