The User Interfaces for Theorem Provers workshop 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.
The workshop 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.

ENTCS Volume

Selected, revised papers from the UITP 2003 workshop will appear as Volume 103 of Electronic Notes in Theoretical Computer Science. The volume is currently prepared for publication now; as soon as it appears on ENTCS web site we will link it from here.

Here are the papers that will appear in this volume:

UITP 2003

UITP 2003 was held as a one-day workshop on Monday 8th September 2003, in conjunction with TPHOLS 2003.


9.00      Welcome

9.15 Visualizing geometrical statements with GeoView
Yves Bertot, Frédérique Guilhot and Loïc Pottier
9.45 Proving as Programming with DrHOL: A Preliminary Design.
Scott Owens and Konrad Slind
10.30 Coffee & demos
11.00 Interactive Disproof
Rendering Tree Proofs in Box Form
Richard Bornat
11.30 Formal Proof Authoring: an Experiment
Laurent Thery
12.00 Proof General meets IsaWin
David Aspinall and Christoph Lüth
12.30 Lunch
14.00 TeXMacs as Authoring Tool for Publication and Dissemination of Formal Developments
Philippe Audebaud and Laurence Rideau
14.30 Interactive Proof Construction at the Task Level
Malte Huebner, Christoph Benzmueller, Serge Autexier, Andreas Meier
15.00 User Interface for Adaptive Suggestions for Interactive Proof
Martin Pollet, Erica Melis, Andreas Meier
15.30 Coffee & demos
16.00 Taclets and the KeY Prover
Martin Giese
16.30 Improving the PVS User Interface
Joseph R. Kiniry
17.00 Thoughts on Requirements and Design of User Interfaces for Proof Assistants
Norbert Völker
17.30      Closing

A copy of the proceedings as distributed at the meeting is available here (PDF format).

Programme committee:

The organisers of UITP'03 are Christoph Lüth and David Aspinall.

UITP 2005

The next workshop on User Interfaces for Theorem Provers UITP'05 will be held as a satellite workshop of ETAPS'05 on April 9th, 2005 in Scotland's beautiful capital, Edinburgh.

For more details, see the workshop page.

Previous UITP meetings

Previous meetings were held annually from 1995-1998, organised principally by Tom Melham in connection with a research project at the University of Glasgow which aimed to apply HCI research methods and results to theorem prover interfaces.