[Agda] [Fwd: [Types] User Interfaces for Theorem Provers UITP05 -- Call for Papers]

[Andreas Abel]

Has anyone written a paper about interactive proving in Agda yet?  If 
not, here is a workshop:

-------- Original Message --------
Subject: [Types] User Interfaces for Theorem Provers UITP05 -- Call for 
Papers
Date: Thu, 09 Dec 2004 16:46:14 +0000
From: David Aspinall <uitp05 at inf.ed.ac.uk>
To: puml-list at cs.york.ac.uk, bforum at estas1.inrets.fr, 
zforum at prg.ox.ac.uk, vdm-forum at JISCMAIL.AC.UK, members at fmeurope.org, 
formal-methods at cs.utoronto.ca, formal-methods at cs.uidaho.edu, 
facs at lboro.ac.uk, cs-logic at cs.indiana.edu, 
isabelle-users at cl.cam.ac.uk, info-hol at jaguar.cs.byu.edu, 
types at lists.chalmers.se, pvs at csl.sri.com, theorem-provers at ai.mit.edu, 
coq-club at pauillac.inria.fr, qed at mcs.anl.gov, rewriting at ens-lyon.fr

[ Apologies if you receive multiple copies.  NB: the deadline has
changed since the initial advertisements appeared on the web! ]



                         CALL FOR PAPERS

           User Interfaces for Theorem Provers, UITP 2005

                 A Satellite Workshop of ETAPS 2005
           Edinburgh (Scotland),  Saturday 9th April 2005

                   http://uitp05.inf.ed.ac.uk/

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 2005 is a one-day workshop to be held on Saturday 9th April 2005
2003 in Edinburgh, Scotland, as a satellite workshop of ETAPS 2005.


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.

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

Authors are encouraged to bring along versions of their systems
suitable for informal demonstration during breaks in the programme of
talks.

After the workshop, there will be the opportunity to submit extended
and revised papers to a dedicated volume in the Elsevier Electronic
Notes in Theoretical Computer Science.


Dates

  Deadline for submissions:  14th January 2005
  Notification:              14th February 2005
  Final versions due:        4th  March 2005
  Workshop:                  9th April 2005


Submission instructions

Please send your paper in Postscript or PDF format to

		uitp05 at inf.ed.ac.uk

We will acknowledge submissions.  If you do not hear within a few days
of submitting, please send a note in plain text.  Please use the same
email address for any queries.

More information can be found on the UITP web page at
http://uitp05.inf.ed.ac.uk/.


Programme Committee

   David Aspinall   (Edinburgh, UK, organiser)
   Christoph Lüth   (Bremen, Germany, organiser)
   Yves Bertot      (Sophia, France)
   Richard Bornat   (Middlesex, UK)
   Paul Cairns      (London, UK)
   Erica Melis      (Saarbrücken, Germany)
   Burkhart Wolff   (Zürich, Switzerland)
_______________________________________________
Types mailing list
Types at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/types

-- 
Andreas Abel  <><      --<>--     Du bist der geliebte Mensch.

Dept. of Computer Science,   Chalmers University of Technology
Rännvägen 6, rum 5111A, 41296 Göteborg, SWEDEN, +46-31-7721006