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 2008 is a one-day workshop to be held on Friday, August 22nd 2008
in Montreal, Canada, as a
TPHOLS'08 workshop.
Schedule
Regular Session 1
- 9:00-09:30 Enrico Tassi and Andrea Asperti. An interactive driver for goal directed proof strategies
- 9:30-10:00 Claudio Sacerdoti Coen. User Interfaces for Mathematical Systems that Allows Ambiguous Formulae.
Regular Session 2
- 10:30-11:00 Holger Gast. Managing Proof Documents for Asynchronous Processing (slides).
- 11:00-11:30 David Aspinall, Serge Autexier, Christoph Lüth and Marc
Wagner. Towards Merging Plato and PGIP (slides).
- 11:30-12:00 Julien Charles and Joseph Kiniry. A Lightweight Theorem Prover Interface for Eclipse.
Regular Session 3
- 14:00-14:30 John Byrnes, Michael Buchanan, Michael Ernst, Philip Miller,
Chris Roberts and Robert Keller. Visualizing Proof Search for Theorem Prover
Development.
- 14:30-15:00 William Farmer and Orlin Grigorov. Panoptes: An Exploration
Tool for Formal Proofs.
- 15:00-15:30 Paulo Pinheiro da Silva, Nicholas Del Rio, Deborah McGuinness,
Li Ding, Cynthia Chang and Geoff Sutcliffe. User Interfaces for Portable
Proofs.
Invited System Demonstrations
- 16:00-16:30 (Invited Demonstration I) Matt Kaufmann. Interface aspects of
the ACL2 theorem proving system. (joint work with J Strother Moore)
(Demo
abstract, Demo material)
- 16:30-17:00 (Invited Demonstration II) Sam Owre. A Brief Overview of the
PVS User Interfaces. (Demo abstract)
- 17:00 Deborah McGuinness. Inference Web and TPTP.
(Demo abstract)
The informal workshop proceedings can be found
here.
Important dates
- Submission deadline: May 25th, 2008 (extended)
- Acceptance notification: June 27th, 2008
- Camera-ready copy: August 4th, 2008
Programme Committee
- David Aspinall, University of Edinburgh, Scotland
- Serge Autexier, Saarland University and DFKI Saarbrücken, Germany (Co-Chair)
- Chris Benzmüller, Saarland University, Germany (Co-Chair)
- Yves Bertot, INRIA Sophia-Antipolis, France
- William Billingsley, University of Cambrigde, England
- Paul Cairns, University College London, England
- Ewen Denney, NASA Ames Research Center, USA
- Herman Geuvers, Radboud University Nijmegen, The Netherlands
- Christoph Lüth, University of Bremen and DFKI Bremen, Germany
- Michael Norrish, NICTA, Australia
- Claudio Sacerdoti-Coen, University of Bologna, Italy
- Gem Stapleton, University of Brighton, England
- Geoff Sutcliffe, University of Miami, USA
- Makarius Wenzel, TU Munich, Germany
If you have any questions about the workshop, please contact the
organizers: uitp08@ags.uni-sb.de.
More information about the workshop series can be found at the
UITP Interest Group webpage.
