The Coq mailing list

[Christoph Lueth <cxl AT informatik.uni-bremen.de>]

[Apologies for multiple copies. Feel free to redistribute this call to
any interested parties. -- cxl.]

                         Call for Papers

                  Journal of Automated Reasoning
       Special Issue on User Interfaces for Theorem Proving


With improving technology, theorem proving and related methods are
being applied to larger problems and used in more domains.  Providing
effective and usable interfaces for these tools has been an important
research goal in recent years, and developments have been reported
both in dedicated workshop series and in more general conferences.
To further disseminate results in this area, a special issue of the
Journal of Automated Reasoning dedicated to user interfaces for
theorem proving is planned.

We invite submission of articles describing work on interfaces for
reasoning tools.  Submitted papers should be mature journal articles.
They may address any aspect of the design, implementation and
evaluation of interfaces for theorem proving tools considered in a
general sense, so possible interfaces include those for mathematical
proof assistants, semi-automated provers, interactive model checking
tools, formal method tools, computer algebra systems, etc. Suggested
topics include, but are not limited to:

 * Novel interaction mechanisms or innovative designs for prover interfaces;
 * HCI experiments and evaluation of prover interfaces;
 * Languages and tools for authoring and presenting human-readable proof;
 * Implementation techniques (e.g. web services, custom middleware, DSLs);
 * Integration of interfaces and tools to explore and construct proof;
 * Representation and manipulation of mathematical knowledge or objects;
 * Visualisation of mathematical objects and proof.



Submission format:
==================

Submissions should be written on general terms understandable by the usual
audience of the journal.  They will be refereed to usual journal standards.

Submissions should be formatted according to JAR's author guidelines
(see the link on the home page below), and preferably be written
in LaTeX. A LaTeX style file can be obtained here:

     http://www.springeronline.com/authors/jrnlstylefiles

Dates:
======

Submission ..... Dec 1st, 2005
Notification ... Mar 1st, 2006
Revisions ...... May 1st, 2006
Final version .. Jul 1st, 2006


Websites and Submission procedure:
==================================

Please send the abstract, containing authors names, title and
the paper abstract in plain text, and the full paper in PS or PDF
format as an attachment, to the following address by Dec 1st:

      
uitp AT informatik.uni-bremen.de

Please feel free to send any questions or inquiries to this address as
well.  The website for this special issue, containing more useful
information, will be found at

     http://www.informatik.uni-bremen.de/~cxl/uitp-jar


Deepak Kapur.
Editor-in-Chief,
Journal of Automated Reasoning
David Aspinall, Christoph Lüth.
Guest Editors.