[Prev][Next][Index][Thread]

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


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

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: http://www.cs.york.ac.uk/~nam/uitp/proceedings.html

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 uitp-request@dcs.gla.ac.uk. Messages can be
posted to the list at uitp@dcs.gla.ac.uk. 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

Submissions

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

     Yves.Bertot@sophia.inria.fr

or as four paper copies to

     Yves Bertot
     UITP '97
     INRIA Sophia Antipolis,
     2004, Route des Lucioles, B.P. 93,
     06902 Sophia Antipolis Cedex,
     FRANCE

The call for papers is also available as postscript.

Dates

 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

   * 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

Location

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.

Organiser

Yves Bertot