User Interfaces for Theorem Provers
UITP 2006
August 21, Seattle, Washington, USA
The UITP'06 Workshop is affilliated with IJCAR'06 at FLOC'06

********** Extended Submission Deadline: Wednesday, May 24 **********

The User Interfaces for Theorem Provers workshop 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. The workshop provides a forum for all those interested in improving human interaction and usability of 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.

Here is the list of previous UITP workshps:

Call for Papers

Please find here the official CFP for UITP'06.


Format of the Workshop

The proposed format of the workshop is one day of presentations. In addition the program might include space for demo sessions on attendees' laptops and/or an invited talk.

Program Committee

David Aspinall University of Edinburgh, UK
Yves Bertot INRIA Sophia Antiplois, France
Paul Cairns University College London, UK
Ewen Denney NASA Ames Research Center, USA
Christoph Lüth University of Bremen, Germany
Michael Norrish NICTA, Australia
Florina Piroi RICAM, Austrian Academy of Sciences, Austria
Aarne Ranta Chalmers University, Sweden
Makarius M. M. Wenzel Technical University Munich, Germany

Organizers and PC Chairs

Serge Autexier DFKI, Stuhlsatzenhausweg 3, D-66123 Saarbrücken, Germany.
Christoph Benzmüller FR 6.2 Informatik, Saarland University, D-66041 Saarbrücken, Germany.

If you have any questions about the workshop, please contact the organizers:


Paper can be submitted in PDF format (10-20 pages following ENTCS guidelines) via EasyChair (thanks to Andrei Voronkov).

All papers will be reviewed by members of the Programme Committee and selected by the organizers in accordance with the referee reports.

Important Dates


The workshop proceedings will be distributed at the workshop as a collection of the accepted papers. Final versions of accepted papers have to be prepared with LaTeX. Following up the workshop the (revised) accepted papers will be published in a volume of ENTCS devoted to the workshop.

This page has been created with TeXmacs and is also available as pdf.