AnnotatedBibliography < PG

PG Web>AnnotatedBibliography (11 Sep 2006, HuaYang ) (raw view)EditAttach
---+ Annotated Bibliography of Related Work

%P%: _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.

   * [[http://www.dcs.gla.ac.uk/~stuart/ITP/jsc-paper.ps][Interactive Theorem Proving: An Empirical Study of User Activity.]]<br/>
      by J. S. Aitken, P. Gray, T. Melham and M. Thomas <br/>
      the Journal of Symbolic Computation, November 1995 <br/>

   * [[http://www.dcs.gla.ac.uk/~stuart/ITP/uitp96-paper.ps][Phases, Modes and Information Flow in Theory Development]]<br/>
      by Stuart Aitken, Phil Gray, Tom Melham, and Muffy Thomas <br/>
      Proceedings of User Interface Design for Theorem Provers 1996, (ed) Nicholas Merriam, York, 19 July 1996, pp. 1-8. <br/>

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

-----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
   
   * [[ftp://ftp-sop.inria.fr/croap/General/sde5.ps][Real Theorem Provers Deserve Real User-Interfaces]] <br/>
      by Laurent Théry, Yves Bertot, and Gilles Kahn <br/>
      The Fifth ACM Symposium on Software Development Environments (SDE5), Washington D. C., December 1992. Also appears as Inria Research Report no. 1684, May 1992. <br/>

   * [[ftp://ftp-sop.inria.fr/lemme/Yves.Bertot/pbp.ps][Proof by Pointing]] <br/>
      by Yves Bertot, Gilles Kahn, and Laurent Théry <br/>
      Symposium on Theoretical Aspects Computer Software (STACS), Sendai (Japan), LNCS 789, April 1994. Also appears as Cambridge University Research Report, December 1993. <br/>

   * [[ftp://ftp-sop.inria.fr/lemme/Yves.Bertot/jsymcomp.ps.gz][A Generic Approach to Building User Interfaces for Theorem Provers]] <br/>
      by Yves Bertot and Laurent Théry <br/>
      the Journal of Symbolic Computation Vol. 25, pp. 161-194, 1998 <br/>

   * [[http://www.inria.fr/rapports/sophia/RR-4052.html][Dependency graphs for interactive theorem provers]] <br/>
      by Yves Bertot and Olivier Pons and Loïc Pottier <br/>
      INRIA Research Report RR-4052, November 2000. <br/>

------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
   * [[ftp://ftp-sop.inria.fr/pub/croap/opons/uitp98.ps][Undoing ans managing a Proof]] <br/>
      by Oliver Pons <br/>
      the User Interfaces for Theorem Provers, 1997. <br/>

   * [[ftp://ftp-sop.inria.fr/pub/croap/opons/articleUITP.ps.gz][Notions of dependency in proof assistants]] <br/>
      by Olivier Pons, Yves bertot, Laurence Rideau <br/>
      the User Interfaces for Theorem Provers, 1998. <br/>

   * [[ftp://ftp-sop.inria.fr/lemme/Olivier.Pons/tphol.ps.gz][Proof engineering]] <br/>
      by Olivier Pons <br/>
      INRIA Research Report, February 00/19 2000 . <br/>

   * [[ftp://ftp-sop.inria.fr/lemme/Olivier.Pons/generalisation.ps.gz][Proof reuse generalization and proof ]] <br/>
      by Olivier Pons <br/>
      TPHOL, August 2000. <br/>
Topic revision: r2 - 11 Sep 2006 - 09:09:22 - HuaYang
Copyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback
This Wiki uses Cookies