The User Interfaces for Theorem Provers workshop brings
together researchers interested in designing, developing and
evaluating interfaces for interactive proof systems, including
(but not limited to) theorem provers, formal method tools, and
other tools manipulating and presenting proofs.
While the reasoning capabilities of interactive proof
tools 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 was held on Saturday 9th April 2005 in Edinburgh, Scotland, as a satellite workshop of ETAPS 2005.
| 9.00 | Graham Steel: Visualizing First-Order Proof Search |
| 09:30 | Andrew Cook and Andrew Ireland: Proof Animation |
| 10:00 | Lucas Dixon: Interactive Hierarchical Tracing of Techniques in IsaPlanner |
| 10:30 | Coffee break |
| 11:00 | Jacques Fleuriot and Sean Wilson: Combining Dynamic Geometry, Automated Geometry Theorem Proving and Diagrammatic Proofs |
| 11:30 | Martin Homik and Andreas Meier: Designing a Proof GUI for Non-Experts: Evaluation of an Experiment. |
| 12:00 | Mark Buckley and Christoph Benzmüller: System Description: A Dialogue Manager supporting Natural Language Tutorial Dialogue on Proofs |
| 12:30 | Lunch |
| 14:00 | Serge Autexier, Christoph Benzmüller, Armin Fiedler and Henri Lesourd: Integrating Proof Assistants as Reasoning and Verification Tools into a Scientific WYSIWIG Editor. |
| 14:30 | Catarina Coquand, Dan Synek and Makoto Takeyama: An Emacs Interface for Type-Directed Support for Constructing Proofs and Programs |
| 15:00 | David Aspinall, Christoph Lüth and Daniel Winterstein: Parsing, Editing, Proving: The PGIP Display Protocol |
| 15:30 | Coffee |
| 16:00 | Daniel Winterstein, David Aspinall and Christoph Lüth: Proof General / Eclipse: A Generic Interface for Interactive Proof |
| 16:30 | Dominik Haneberg: The User Interface of the KIV Verifcation System: A System Description |
| 17:00 | Ewen Denney and Bernd Fischer: A Program Certification Assistant Based on Fully Automated Theorem Provers |
| 17:30 | System demonstrations |
Submissions of revised papers are being accepted for the ENTCS volume associated with the meeting. Submission is open to the authors of presented papers.
Please send papers in PDF format to uitp05@inf.ed.ac.uk. We will acknowledge submissions. If you do not hear within a few days of submitting, please send a note in plain text. Papers will be reviewed by members of the Programme Committee, listed below.
| Submission of ENTCS version: | 16th May 2005 |
| Reviews returned: | 5th August 2005 (NB: re-re-adjusted date, apologies!) |
| Final ENTCS versions: | 9th November 2005 (NB: also doubly re-adjusted date) |
For the final ENTCS versions we require LaTeX sources using the ENTCS syle files as described here, using the UITP version of prentcsmacro.sty. We also need a filled in copy of the template.txt file and a scanned copy of a completed copyright transfer form ctf2.pdf.
Programme committee for UITP 2005:Previous meetings were held in 1995-1998, and 2003.