Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 29 Jun 1995 11:34:42 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA112500669; Thu, 29 Jun 1995 04:11:09 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from vanuata.dcs.gla.ac.uk by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA112460661; Thu, 29 Jun 1995 04:11:01 -0600 Received: from timor.dcs.gla.ac.uk by vanuata.dcs.gla.ac.uk with LOCAL SMTP (PP); Thu, 29 Jun 1995 11:10:11 +0100 Received: by timor.dcs.gla.ac.uk (4.1/Dumb) id AA00638; Thu, 29 Jun 95 11:10:03 BST Date: Thu, 29 Jun 95 11:10:03 BST From: muffy@dcs.gla.ac.uk Message-Id: <9506291010.AA00638@timor.dcs.gla.ac.uk> To: info-hol@leopard.cs.byu.edu, bcs-hci-request@mailbase.ac.uk Subject: ITP Workshop Registration Details Dear Colleague Here follows the draft program and registration details for the Workshop on User Interface Design for Theorem Proving Systems. ======================================================================= International Workshop on User Interface Design for Theorem Proving Systems Department of Computing Science University of Glasgow 18 July 1995 PROGRAMME ~~~~~~~~ 8:40 - 9:00 Welcome 9:00 - 9:40 Invited talk Assessing Theorem Proving Assistants: Concepts and Criteria Nicholas Merriam, Andrew Dearden, Michael Harrison Department of Computer Science, University of York 9:40 - 10:00 User Interface Design for an Automated Pedagogic Tool Jeremy Pitt Department of Computing, Imperial College London 10:00 - 10:20 The User Interface of a Proof Assistant for Z Specifications Ian Toyn Department of Computer Science, University of York 10:20 - 10:40 Diagrams and Human Reasoning Corin Gurr Human Communication Research Centre, University of Edinburgh 10:40 - 11:10 Coffee 11:10 - 11:50 User Interface Principles for Proof Editors Richard Bornat, Bernard Sufrin QMW, University of London Oxford University 11:50 - 12:10 A Co-operative Interface for Theorem Proving Using Proof Plans Helen Lowe, Alan Bundy Department of Computer Studies, Napier University Department of Artificial Intelligence, University of Edinburgh 12:10 - 12:30 Interactive first-order Deduction with BDDs Joachim Posegga, Klaus Schneider Institut fuer Logik, Komplexitaet und Deduktionssysteme, Universitaet Karlsruhe Institut fuer Rechnerentwurf und Fehlertoleranz, Universitaet Karlsruhe 12:30 - 14:00 Lunch and informal discussion 14:00 - 14:40 Invited talk Interactive Proof Discovery: An Empirical Study of HOL Users Stuart Aitken Department of Computing Science, University of Glasgow 14:40 - 15:00 The User Interface and the Proof Process Brian Matthews Systems Engineering, Rutherford Appleton Laboratory 15:00 - 15:20 Presenting Machine-Found Proofs Xiaorong Huang Fachbereich Informatik, Universitaet des Saarlandes 15:20 - 15:50 Tea 15:50 - 16:20 Invited talk A Generic Approach to Building User Interfaces for Theorem Provers Laurent Th{\'e}ry INRIA, Sophia Antipolis 16:20 - 16:40 Interface Projects - Making them succeed Donald Syme Computer Laboratory, University of Cambridge 16:40 - 17:00 Discussion and business session 17:00 - 19:30 Demonstrations 18:30 - 19:30 Drinks 19:30 End of workshop Registration Form ================== I will be attending the workshop on 18 July. ...................................................(Name) ...................................................(Affiliation) The fee for the workshop is 25 pounds and will be payable at the workshop. An invoice can be issued at that time. Please return a completed registration form (by email if possible) to Muffy Thomas (muffy@dcs.gla.ac.uk) by 3 July. Places will be limited so please register early. It may be possible to register on the day, if there are sufficient places. If you need accommodation, there are numerous Bed & Breakfasts and small Hotels near the University. For further details and assistance with booking, please contact helen@dcs.gla.ac.uk.