User Interfaces for Theorem Provers'97 (2nd call for papers)
Many interactive proof systems are based on type theory, and some of
these have made significant efforts to provide elaborate interfaces.
For this reason, this announcement may be of interest to the type
Call for Paper
User Interfaces for Theorem Provers 1997
INRIA Sophia-Antipolis, Monday and Tuesday, 1-2nd September 1997
This page: http://www.inria.fr/croap/events/uitp97.html
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
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
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 firstname.lastname@example.org. Messages can be
posted to the list at email@example.com. 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.
* 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 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
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
* Stuart Aitken
* Roland Backhouse
* David Benion
* Yves Bertot
* Richard Bornat
* Masami Hagiya
* Xiaorong Huang
* Gilles Kahn
* Helen Lowe
* Tom Melham
* Nick Merriam
* Laurent Théry
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