Annotated Bibliography of Related Work

: in progress

An attempt to make a list of important publications related to the field of user interfaces for theorem provers: mainly those with connections to Proof General. Not necessarily complete or unbiased.

• Interactive Theorem Proving: An Empirical Study of User Activity.
  by J. S. Aitken, P. Gray, T. Melham and M. Thomas
  the Journal of Symbolic Computation, November 1995
  

• Phases, Modes and Information Flow in Theory Development
  by Stuart Aitken, Phil Gray, Tom Melham, and Muffy Thomas
  Proceedings of User Interface Design for Theorem Provers 1996, (ed) Nicholas Merriam, York, 19 July 1996, pp. 1-8.
  

• From Notation to Semantics: There and Back Again
  by Luca Padovani, Stefano Zacchiroli
  the Proceedings of the 5th International Conference on Mathematical Knowledge Management (MKM'06), Wokingham, UK, August 2006
  

• Real Theorem Provers Deserve Real User-Interfaces
  by Laurent Théry, Yves Bertot, and Gilles Kahn
  The Fifth ACM Symposium on Software Development Environments (SDE5), Washington D. C., December 1992. Also appears as Inria Research Report no. 1684, May 1992.
  

• Proof by Pointing
  by Yves Bertot, Gilles Kahn, and Laurent Théry
  Symposium on Theoretical Aspects Computer Software (STACS), Sendai (Japan), LNCS 789, April 1994. Also appears as Cambridge University Research Report, December 1993.
  

• A Generic Approach to Building User Interfaces for Theorem Provers
  by Yves Bertot and Laurent Théry
  the Journal of Symbolic Computation Vol. 25, pp. 161-194, 1998
  

• Dependency graphs for interactive theorem provers
  by Yves Bertot and Olivier Pons and Loïc Pottier
  INRIA Research Report RR-4052, November 2000.
  

• Undoing ans managing a Proof
  by Oliver Pons
  the User Interfaces for Theorem Provers, 1997.
  

• Notions of dependency in proof assistants
  by Olivier Pons, Yves bertot, Laurence Rideau
  the User Interfaces for Theorem Provers, 1998.
  

• Proof engineering
  by Olivier Pons
  INRIA Research Report, February 00/19 2000 .
  

• Proof reuse generalization and proof
  by Olivier Pons
  TPHOL, August 2000.