Title: User Interface Design for Interactive Theorem Provers

  Abstract: 

  The technology of mechanized theorem proving (doing formal proofs by
  computer) is vitally important to the use of formal methods in
  actual software engineering practice.  But one major obstacle to the use
  of this technology is the poor quality of user interface provided by
  many systems.  Although there have been projects to develop good
  interfaces for specific systems, the designers of these interfaces
  have almost universally failed to draw upon modern methods of
  research in Human Computer Interaction.

  This talk will describe some preliminary results obtained as part of
  a project designed to rectify this lack of analysis.  First, some
  thoughts about the interaction between users and a specific
  interactive theorem prover (the HOL system) will be presented.  The
  talk will then present the results of an empirical study of
  intermediate and expert HOL users. The results will be analysed with
  a view to formulating principles of good interface design for
  interactive proof systems.  The talk will be non-technical, and will
  aim merely to introduce this new and exciting area of HCI research.

This will be a warm-up talk for a seminar I'm going to give 
at King's College, London, on 15 November.