User Interfaces for Theorem Provers 1997

INRIA Sophia-Antipolis, Monday and Tuesday, 1-2nd September 1997
[Information en Français] [Postscript version] [Workshop] [Topics] [Submissions] [Dates] [Programme Committee] [Location] [Organiser] [presented papers]
This page:

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

In 1995 the first workshop in this series was hosted at the Department of Computer Science at the University of Glasgow. A brief report was published in FACS Europe.

In 1996 the second workshop was hosted at the University of York.
Electronic proceedings for this workshop are now available at the following address:

There is a mailing list for disseminating information about the workshop series and discussion relevant to user interfaces for theorem provers. To subscribe, email a request to Messages can be posted to the list at All information about the 1997 workshop will be posted there.

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.


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 either be sent electronically, with the cover sheet as the body of an email and the paper as a postscript enclosure, to
or as four paper copies to
Yves Bertot
UITP '97
INRIA Sophia Antipolis,
2004, Route des Lucioles, B.P. 93,
06902 Sophia Antipolis Cedex,
The call for papers is also available as postscript.


Submissions deadline 7th April 1997
Notification of acceptance 16th June 1997
Finished papers 15th July 1997
Intention to register 15th July 1997
Workshop 1-2 September 1997

Programme Committee


The workshop will be held at INRIA Sophia Antipolis in the south of France. This research center is located near Antibes, very close to the Nice airport.


Yves Bertot
Up to the CROAP project home page.
Please send any comments about this web page to