While interactive theorem provers have found many new application areas in 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. More and more, this is becoming an obstacle for the wider adoption of theorem proving technologies outside the academic community.
The User Interfaces for Theorem Provers workshop series provides a forum for researchers interested in improving human interaction with interactive proof systems, be it theorem provers, formal method tools, and other tools manipulating and presenting mathematical formulas.
For the forthcoming 10th UITP workshop, we invite 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:
UITP 2012 was a one-day workshop on July 11th 2012 in Bremen, Germany, as a CICM 2012 workshop.
This is the programme for the workshop. Talks are intended to be twenty minutes long, to leave room for plenty of questions and discussion.
|Theorema 2.0: A Graphical User Interface for a Mathematical Assistant System|
|09:30||Cvetan Dunchev, Alexander Leitsch, Tomer Libal, Martin Riener, Mikheil Rukhaia, Daniel Weller and Bruno Woltzenlogel-Paleo.|
|ProofTool: GUI for the GAPT Framework|
|READ-EVAL-PRINT in Parallel and Asynchronous Proof-Checking|
|Interfacing with Proof Assistants for Domain Specific Programming Using EventML|
|11:30||Andrei Lapets, Richard Skowyra, Christine Bassem, Assaf Kfoury and Azer Bestavros|
|Towards an Infrastructure for Integrated Accessible Formal Reasoning Environments|
|12:00||Mihnea Iancu and Florian Rabe|
|An MMT-Based User-Inteface|
The location of the workshop is the Western Hall on the campus of Jacobs Unversity, where CICM 2012 is taking place; see the CICM webpage.
For the forthcoming post-workshop proceedings, in addition to accepted presentations at the workshop we invite further contributions addressing the topics of UITP 2012 as laid out above.
Submitted papers should describe previously unpublished work, and must be prepared in LaTeX using the EPTCS macro package which can be downloaded from here. There is no strict page limit. Authors are asked to consult the author information with regards to content, format and metadata. Submission will be via EasyChair at this address. All submissions will be peer reviewed by members of the programme committee, and accepted papers will appear in an EPTCS volume.
More information about the workshop series can be found at the UITP Interest Group webpage.