This is the permanent home page of the User Interfaces for Theorem Provers (UITP) workshop series. The UITP 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 formulae.

The UITP workshop series started in 1995 with an international workshop in Glasgow. Apart from a hiatus between 1998 and 2003, the workshop meets roughly every other year.

Next meeting

Preparations are under way for a UITP in 2018. Watch this space.

List of Previous Meetings

  1. UITP'16: July 2nd, Coimbra, Portugal. IJCAR 2016 workshop.
  2. UITP'14: July 17th, Vienna. ITP/IJCAR-workshop at FLoC'14 (part of the Summer of Logic).
  3. UITP'12: July 11th 2012, Bremen. CICM'12 Workshop.
  4. UITP'10: July 15th 2010, Edinburgh. ITP'10 Workshop at FLOC'10.
  5. UITP'08: Aug 22nd 2008, Montréal, Québec, Canada. TPHOLs'08 satellite workshop.
  6. UITP'06: Aug 21st 2006, Seattle. FLoC'06 Satellite Workshop.
  7. UITP'05: Apr 9th 2005, Edinburgh. ETAPS'05 Satellite Workshop.
  8. UITP'03: Sep 8th 2003, Rome. Colocated with TPHOLs 2003.
  9. UITP'98: July 13-15 1998, Eindhoven University of Technology.
  10. UITP'97: Sept 1-2, 1997, Sophia-Antipolis on September, 1-2 1997.
  11. UITP'96: July 19th 1996, University of York.
  12. A one-day International Workshop on User Interface Design for Theorem Proving Systems was held at Glasgow on 18 July 1995. There is an on-line archive of the workshop and a report.

Steering Committee

A group of volunteers is seeking to ensure continuity between meetings:


You can reach us under the following email-adress:

uitp at