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.
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 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.
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 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.