UITP 1998 1st CFP

User Interfaces for Theorem Provers 1998

1st Call for Papers

Eindhoven University of Technology
Monday and Tuesday, 13-14th July 1998 

The Workshop

This international workshop provides a forum for the exchange of ideas and
research on the analysis and design of user interfaces for theorem proving
assistants. In particular it facilitates cross-fertilisation between the
fields of human-computer interaction (HCI) and mechanised theorem proving. 

The series was started in recognition of the fact that the difficulty in
using powerful theorem proving software frequently lies with a poor user
interface. There are gaps between the knowledge required by designers of
such interfaces and present state of the art in general interface design
technology. Effective solutions require the collaboration of HCI
practitioners and the authors and users of existing theorem proving

The first workshop in this series was held in 1995 at the University of
Galsgow; in 1996 the workshop was held at the University of York and in
1997 at INRIA, Sophia Antipolis. Further information on these workshops and
up to date information on the current workshop can be found at

Topics of Interest

The theme of the workshop is the study of interfaces for theorem proving
assistants and all pertinent submissions will be considered. Papers on the
following topics are especially welcome. 

  * Analysis of interfaces 
  * Case studies of tools 
  * Interaction for proof planning 
  * Reading and representation of mathematics/logic 
  * Interaction for reuse (of theorems, etc.) 
  * Studies of reasoning 
  * Interface useability studies 


Papers may be up to 8 pages in length. In addition, system demonstrations
are invited. A cover sheet displaying the author's name, email and postal
addresses, the title and abstract of the paper and whether or not a
demonstration will be on offer, should be included. 

Submissions should be sent electronically, with the cover sheet as the body
of an email and the paper as a postscript enclosure, to 



 Submission deadline          27 March 1998 
 Notification of acceptance   18 May 1998 
 Workshop                     13-14 July 1998 

Programme Committee

  * Stuart Aitken 
  * Roland Backhouse 
  * David Benyon 
  * Yves Bertot 
  * Richard Bornat 
  * Herman Geuvers 
  * Joseph Goguen 
  * Masami Hagiya 
  * Gilles Kahn 
  * Helen Lowe 
  * Tom Melham 
  * Nick Merriam 
  * T. Nakagawa 
  * Steve Reeves 
  * Bernard Sufrin 
  * Laurent Thery 


The workshop will be held at Eindhoven University of Technology the

Invited Speakers and Panel Discussion

We expect to have two invited speakers at the workshop, details of which
will be made known in due course. In addition a number of panel discussions
will be organized.

Related Events

The workshop is being organized in conjunction with the Calculemus workshop
which will also be held at Eindhoven University of Technology in the
Netherlands from 13th to 15th July, 1998. The two workshops will have joint
programmes and participants will be able to attend both. Submission of
papers is however independent.  The Calculemus workshop is devoted to the 
integration and/or linkage of theorem provers and computer algebra systems.


This workshop is sponsored by IPA (Institute for Programming research and