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.
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. Topics covered include, but are not limited to:
- Application-specific interaction mechanisms or designs for prover interfaces
- Experiments and evaluation of prover interfaces
- Languages and tools for authoring, exchanging and presenting 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
- System descriptions
UITP 2010 is a one-day workshop to be held on July 15th 2010
in Edinburgh, Scotland, as a
FLOC'10 workshop.
Registration
Registration is now open.
Participants must register through on the
unified FLOC
registration site. Beware that early registration ends the 17th May and
regular registration the 30th June.
Accepted Presentations
Drafts of the accepted papers
- Makarius Wenzel. Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit
- John Slaney. Visualising Reasoning: What ATP can learn from CP
- Carst Tankink, Herman Geuvers and James McKinna. Narrating Formal Proof (Work in Progress)
- Freek Wiedijk. Pollack-inconsistency
- Holger Gast. Engineering the Prover Interface
- Vladimir Komendantsky, Alexander Konovalov and Steve Linton. Interfacing Coq + SSReflect with GAP
- Tuan Minh Pham and Yves Bertot. A combination of a dynamic geometry software with a proof assistant for interactive formal proofs
- Laura Meikle and Jacques Fleuriot. Integrating Systems around the User: Combining Isabelle, Maple, and QEPCAD in the Prover's Palette
- Andrei Lapets and Assaf Kfoury. A User-friendly Interface for a Lightweight Verification System
Submission (closed)
Submissions are encouraged in one of the following two categories:
Regular paper: Submissions in
this category should describe previously unpublished work
(completed or in progress), including descriptions of
research, tools, and applications. Papers should be formated
following the ENTCS guidelines
and up to 15 pages long (please find here the additional UITP10-specific
ENTCS macro file).
System description: Submissions in this
category are intended to describe existing systems. Papers
should be formated following the ENTCS guidelines and up to 5
pages long (please find here the additional UITP'10-specific ENTCS macro file).
Submission of papers is via EasyChair. All
submissions will be peer reviewed and final versions of
accepted submissions will be published in an ENTCS
volume. Final versions of accepted papers
have to be prepared with LaTeX.
Important dates
- Submission deadline: April 9th, 2010
- Acceptance notification: April 30th, 2010
- Camera-ready copy: May 19th, 2010
Programme Committee
- David Aspinall, University of Edinburgh, Scotland (Co-Chair)
- Serge Autexier, DFKI Bremen, Germany
- Christoph Benzmüller, Saarland University, Germany
- Yves Bertot, INRIA Sophia-Antipolis - Méditerranée, France
- Ewen Denney, NASA Ames Research Center, USA
- Cezary Kaliszyk, Technical University München, Germany
- Paul Libbrecht, University of Saarlandes and DFKI Saarbrücken, Germany
- Christoph Lüth, University of Bremen and DFKI Bremen, Germany
- James McKinna,Radboub University Nijmegen, NL
- Michael Norrish, NICTA, Australia
- Claudio Sacerdoti Coen, University of Bologna, Italy (Co-Chair)
- Geoff Sutcliffe, University of Miami, USA
- Laurent Thery, INRIA Sophia-Antipolis - Méditerranée, France
- Gem Stapleton, University of Brighton, England
- Makarius Wenzel, TU Munich, Germany
- Burkhart Wolff, University Paris-Sud 11, France
If you have any questions about the workshop, please contact the
organizers: uitp10@cs.unibo.it.
More information about the workshop series can be found at the
UITP Interest Group webpage.
