The Coq mailing list

[Christoph Lueth <cxl AT Informatik.Uni-Bremen.DE>]

[Apologies if you receive multiple copies.]


                        CALL FOR PAPERS

           Workshop on User Interfaces for Theorem Provers 
                           
                           UITP 2003

                   Co-located with TPHOLs 2003.

                Rome (Italy), 8. September 2003.


The User Interfaces for Theorem Provers workshop series 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.

While the reasoning capabilities of interactive proof systems have
increased dramatically over the last years, the system interfaces have
often not enjoyed the same attention as the proof engines themselves.
In many cases, interfaces remain relatively basic and under-designed.
Initial studies by HCI (Human-Computer Interaction) practitioners and
theorem-prover developers working in collaboration have had promising
early results, but much remains to be investigated.

The User Interfaces for Theorem Provers workshop series 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.

UITP 2003 is a one-day workshop to be held on Monday 8th September
2003 in Rome (Italy), in conjunction with TPHOLs 2003.


Submissions
~~~~~~~~~~~

We encourage submission of short abstracts or papers (from 4-20
pages). Submissions will be reviewed by the programme committee. We
will invite authors of accepted submissions to talk at the workshop
(slots of 20-30 minutes are expected). Submissions presented at the
workshop will be included in informal proceedings to be distributed at
the workshop and made available electronically afterwards.
Additionally, it is planned to publish selected submissions of
sufficiently high quality in an electronic journal. Suggested topics
include, but are not restricted to:

    * Novel interfaces for interactive proof systems
    * Design principles for interfaces
    * Proof development languages and environments
    * User-evaluation of interfaces
    * Integration of interfaces and tools
    * Web-based services for proof systems
    * Implementation experiences
    * System descriptions

It is planned to devote one session to system
demonstrations. Prospective demonstrators should submit a short
description (from 2- 4 pages) of the system, if the demonstration is
not part of a normal paper.


Dates:
~~~~~~

Deadline for submissions: 1st June 2003
Notification:             21st June 2003
Final versions due:       1st August 2003

Submission instructions: 

Please send your paper in Postscript or PDF format to

      
uitp03 AT informatik.uni-bremen.de


Programme committee:
~~~~~~~~~~~~~~~~~~~~

    * Christoph Lüth    
<cxl AT informatik.uni-bremen.de>
    * David Aspinall    
<da AT dcs.ed.ac.uk>
    * Tom Melham        
<Tom.Melham AT comlab.ox.ac.uk>
    * Yves Bertot       
<Yves.Bertot AT sophia.inria.fr>
    * Erica Melis       
<melis AT dfki.de>
    * Burkhart Wolff    
<wolff AT informatik.uni-freiburg.de>
    * Stuart Aitken     
<stuart AT inf.ed.ac.uk>

The organisers of UITP'03 are Christoph Lüth and David Aspinall.