12th International Workshop on User Interfaces for Theorem Provers
IJCAR 2016 Satellite Workshop
Saturday, July 2nd, 2016, Coimbra, Portugal
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:

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
16:35-17:10 Christoph Lüth. Hands-on Cobra
17:10-17:45 Emilio Jesus Gallego Arias. Hands-On jsCoq
17:45-18:00Closing Remarks


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

Programme Committee

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.