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.

Programme for UITP 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:30Coffee break
11:00Jacques Fleuriot and Sean Wilson:
Combining Dynamic Geometry, Automated Geometry Theorem Proving and Diagrammatic Proofs
11:30Martin Homik and Andreas Meier:
Designing a Proof GUI for Non-Experts: Evaluation of an Experiment.
12:00Mark 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:30Catarina Coquand, Dan Synek and Makoto Takeyama:
An Emacs Interface for Type-Directed Support for Constructing Proofs and Programs
15:00David 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:30System demonstrations

Submissions for ENTCS volume

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 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 UITP meetings

Previous meetings were held in 1995-1998, and 2003.