NEWS: The programme is now online here

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 2016 is a one-day workshop to be held on Saturday, July 2nd, 2016 in Coimbra, Portugal, as a IJCAR 2016 workshop.

Invited Speaker

This year's workshop will have Sylvain Conchon as invited speaker giving a talk on "AltGr-Ergo, a graphical user interface for the SMT solver Alt-Ergo".

Program (subject to minor changes)

9:15	Welcome
9:30-10:30	Invited Talk: Sylvain Conchon. AltGr-Ergo, a graphical user interface for the SMT solver Alt-Ergo
10:30-11:00	Coffee Break
11:00-11:30	Sven Linker, Jim Burton and Mateja Jamnik. Tactical Diagrammatic Reasoning
11:30-12:00	Emilio Jesus Gallego Arias, Benoit Pin and Pierre Jouvelot. jsCoq: Towards a Hybrid Theorem Proving Interface for Coq
12:00-12:30	Shuai Wang. ProofCloud: A Proof Retrieval Engine for Verified Proofs in Higher Order Logic
12:30-14:00	Lunch
14:00-14:30	Martin Ring and Christoph Lüth. Interactive Proof Presentations with Cobra
14:30-15:00	John Slaney and Nursulu Kuspanova. Why there is no solution: A diagnosis tool for teaching logic
	*Hands-On Demos I*
15:00-15:35	Sven Linker. Hands-on Tactical Diagrammatic Reasoning with SpeedIth
15:35-16:00	Coffee Break
	*Hands-On Demos II*
16:00-16:35	Christoph Benzmüller. Hands-on Higher-order Modal Logics in Isabelle/HOL
	*Hands-On Demos I*
17:10-17:45	Emilio Jesus Gallego Arias. Hands-On jsCoq
17:45-18:00	Closing Remarks

Proceedings

Authors will have the opportunity to incorporate feedback and insights gathered during the workshop to improve their accepted papers before publication in the post-proceeding in the Electronic Proceedings in Theoretical Computer Science (EPTCS - http://www.eptcs.org/).

Important dates

• Submission deadline: May 17th, 2016
• Acceptance notification: June 6th, 2016
• Workshop: July 2nd, 2016

Programme Committee

• Serge Autexier, DFKI Bremen, Germany (Co-Chair)
• Pedro Quaresma, U Coimbra, Portugal (Co-Chair)
• David Aspinall, University of Edinburgh, Scotland
• Chris Benzmüller, FU Berlin, Germany & Stanford, USA
• Yves Bertot, INRIA Sophia-Antipolis, France
• Gudmund Grov, Heriott-Watt University, Scotland
• Zoltán Kovács, RISC, Austria
• Mateja Jamnik, Cambridge, UK
• Christoph Lüth, University of Bremen and DFKI Bremen, Germany
• Alexander Lyaletski, Kiev National Taras Shevchenko University, Ukraine
• Michael Norrish, NICTA, Australia
• Andrei Paskevich, LRI, France
• Gem Stapleton (U Brighton, UK)
• Christian Sternagel, University Innsbruck, Austria
• Enrico Tassi, INRIA Sophia-Antipolis, France
• Laurent Théry, INRIA Sophia-Antipolis, France
• Makarius Wenzel, Sketis, Germany
• Wolfgang Windsteiger, RISC Linz, Austria
• Bruno Woltzenlogel Paleo, TU Vienna, Austria

If you have any questions about the workshop, please contact the co-chairs.

More information about the workshop series can be found at the UITP Interest Group webpage.