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.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|
Rendering Tree Proofs in Box Form
|11.30||Formal Proof Authoring: an Experiment
|12.00||Proof General meets IsaWin
David Aspinall and Christoph Lüth
|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
|16.30||Improving the PVS User Interface
Joseph R. Kiniry
|17.00||Thoughts on Requirements and Design of User Interfaces for Proof Assistants
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.