References

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 http://dx.doi.org/10.1007/3-540-46419-0_3.
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 http://dx.doi.org/10.1007/11532231_7.
3. David A. Basin (1994): Generalized Rewriting in Type Theory. Elektronische Informationsverarbeitung und Kybernetik 30(5/6), pp. 249–259. Available at http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.48.3314.
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 http://dx.doi.org/10.1007/3-540-57887-0_94.
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 http://dx.doi.org/10.1007/978-3-642-16690-7_6.
7. Andrew Butterfield (2012): The Logic of U--(TP)^2, pp. 124–143. Available at http://dx.doi.org/10.1007/978-3-642-35705-3_6.
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 http://dx.doi.org/10.1007/978-3-642-27705-4_20.
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 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.30.9511.
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 http://www.springer.com/computer/theoretical+computer+science/book/978-3-540-43376-7.
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 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.42.1864.
17. Mark Staples (1995): Window Inference in Isabelle. Available at http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.104.6012.
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 http://www3.oup.co.uk/logcom/hdb/Volume_11/Issue_04/110623.sgm.abs.html.
19. Freek Wiedijk (2006): The Seventeen Provers of the World, Foreword by Dana S. Scott. Lecture Notes in Computer Science 3600. Springer. Available at http://www.springer.com/computer/ai/book/978-3-540-30704-4.
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: eptcs@eptcs.org

For website issues: webmaster@eptcs.org