1. David Aspinall (2000): Proof General: A Generic Tool for Proof Development. In: Susanne Graf & Michael I. Schwartzbach: TACAS, LNCS 1785. Springer, pp. 38–42. Available at
  2. Serge Autexier (2005): The CoRe Calculus. In: Robert Nieuwenhuis: Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings, Lecture Notes in Computer Science 3632. Springer, pp. 84–98. Available at
  3. David A. Basin (1994): Generalized Rewriting in Type Theory. Elektronische Informationsverarbeitung und Kybernetik 30(5/6), pp. 249–259. Available at
  4. Yves Bertot & P. (Pierre) Castéran (2004): Interactive theorem proving and program development: Coq'Art: the calculus of inductive constructions. Texts in theoretical computer science. Springer Verlag, doi:10.1007/978-3-662-07964-5.
  5. Yves Bertot, Gilles Kahn & Laurent Théry (1994): Proof by Pointing. In: Masami Hagiya & John C. Mitchell: Theoretical Aspects of Computer Software, International Conference TACS '94, Sendai, Japan, April 19-22, 1994, Proceedings, LNCS 789. Springer, pp. 141–160. Available at
  6. Andrew Butterfield (2010): Saoithin: A Theorem Prover for UTP. In: Shenchao Qin: Unifying Theories of Programming, Third International Symposium, UTP 2010, Shanghai, China, November, 2010., LNCS 6445. Springer, Shanghai, China, pp. 137–156. Available at
  7. Andrew Butterfield (2012): The Logic of U--(TP)^2, pp. 124–143. Available at
  8. Abderrahmane Feliachi, Marie-Claude Gaudel & Burkhart Wolff (2012): Isabelle/Circus: A Process Specification and Verification Environment. In: Rajeev Joshi, Peter Müller & Andreas Podelski: Verified Software: Theories, Tools, Experiments - 4th International Conference, VSTTE 2012, Philadelphia, PA, USA, January 28-29, 2012. Proceedings, Lecture Notes in Computer Science 7152. Springer, pp. 243–260. Available at
  9. Simon Foster, Frank Zeyda & Jim Woodcock (to appear): Isabelle/UTP: A mechanised theory engineering framework. In: David Naumann: Unifying Theories of Programming, Fifth International Symposium, UTP 2014, National University of Singapore, May 13, 2014,.
  10. David Gries & Fred B. Schneider (1993): A Logical Approach to Discrete Math. Texts and Monographs in Computer Science. Berlin: Springer Verlag, doi:10.1007/978-1-4757-3837-7.
  11. Eric C. R. Hehner (1984): Predicative programming — Part I+.1667em&+.1667emII. Commun. ACM 27(2), pp. 134–151, doi:10.1145/69610.357990.
  12. C. A. R. Hoare & Jifeng He (1998): Unifying Theories of Programming. Prentice-Hall.
  13. Dieter Hutter & Claus Sengler (1996): The Graphical User Interface of INKA. In: Nicholas A. Merriam: Proceedings International Workshop on User Interfaces for Theorem Provers. N. Merriam, pp. 43–50. Available at
  14. Tobias Nipkow, Lawrence C. Paulson & Markus Wenzel (2002): Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science 2283. Springer. Available at
  15. Natarajan Shankar (1996): PVS: Combining Specification, Proof Checking, and Model Checking. In: Mandayam K. Srivas & Albert John Camilleri: Formal Methods in Computer-Aided Design, First International Conference, FMCAD '96, LNCS 1166. Springer, pp. 257–264, doi:10.1007/BFb0031813.
  16. Jörg Siekmann, Stephan Hess, Christoph Benzmüller, Lassaad Cheikhrouhou, Armin Fiedler, Helmut Horacek, Michael Kohlhase, Karsten Konrad, Andreas Meier, Erica Melis, Martin Pollet & Volker Sorge (1999): LOmegaUI: Lovely OMEGA User Interface. Available at
  17. Mark Staples (1995): Window Inference in Isabelle. Available at
  18. George Tourlakis (2001): On the Soundness and Completeness of Equational Predicate Logics. J. Log. Comput. 11(4), pp. 623–653, doi:10.1093/logcom/11.4.623. Available at
  19. Freek Wiedijk (2006): The Seventeen Provers of the World, Foreword by Dana S. Scott. Lecture Notes in Computer Science 3600. Springer. Available at
  20. Frank Zeyda & Ana Cavalcanti (2008): Encoding Circus Programs in ProofPower-Z. In: Andrew Butterfield: Unifying Theories of Programming, Second International Symposium, UTP 2008, Trinity College, Dublin, Ireland, September 8-10, 2008, Revised Selected Papers, Lecture Notes in Computer Science 5713. Springer, pp. 218–237, doi:10.1007/978-3-642-14521-6\voidb@x 0.06emwidth0.5em13.

Comments and questions to:
For website issues: