9. L. C. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and Computer Science, pages 361–385. Academic Press, 1990.
10. Lawrence C. Paulson. A Fixed Point Approach to Implementing (Co)inductive Definitions. 18th International Conference on Automated Deduction, pages 148–161, 1994.
4. M.J.C Gordon and T.F Melham. Introduction to HOL: A Theorem Proving Assistant for Higher Order Logic. Cambridge University Press, 1993.
1. Juanito Camilleri and Tom Melham. Reasoning with inductively defined relations in the HOL theorem prover. Technical Report 265, University of Cambridge Computer Laboratory, Cambridge, CB2 3QG, U.K., August 1992.
2. Sophia Drossopoulou and Susan Eisenbach. Is the Java type system sound? (version 2.01). Technical report, Imperial College, University of London, Cambridge, CB2 3QG, U.K., January 1997. This version was distributed on the Internet. Please contact the authors if a copy is required for reference.
7. D. W. Loveland. Mechanical Theorem Proving by Model Elimination. Journal of the ACM, 15:236–251, 1968.
11. Roly Perera and Peter Bertelsen. The Unoffcial Java Bug Report, June 1997. Published on the WWW at http://www2.vo.lu/homepages/gmid/java.htm.
6. John R. Harrison. Proof Style. Technical Report 410, University of Cambridge Computer Laboratory, Cambridge, CB2 3QG, U.K., January 1997.
13. Zhenyu Qian. A Formal Specification of Java Virtual Machine Instructions. Technical report, UniversitÄt Bremen, FB3 Informatik, D-28334 Bremen, Germany, November 1997.
3. James Gosling, Bill Joy, and Guy Steele. The Java Language Specification. Addison-Wesley, 1996.
8. S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M.K. Srivas. PVS: Combining specification, proof checking and model checking. In Rajeev Alur and Thomas A. Henzinger, editors, Computer-Aided Verification, CAV’ 96, volume 1102, pages 411–414. Springer-Verlag, July/August 1996.
14. P. Rudnicki. An Overview of the MIZAR Project, 1992. Unpublished; available by anonymous FTP from menaik.cs.ualberta.ca as pub/Mizar/Mizar_Over.tar.Z. 15. Don Syme. DECLARE: A prototype declarative proof system for higher order logic. Technical Report 416, University of Cambridge Computer Laboratory, Cambridge, CB2 3QG, U.K., March 1997.
5. John Harrison. HOL light: A tutorial introduction. In Mandayam Srivas and Albert Camilleri, editors, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (FMCAD’96), volume 1166 of Lecture Notes in Computer Science, pages 265–269. Springer-Verlag, 1996.
12. Gordon D. Plotkin. A structural approach to operational semantics. Technical report, Computer Science Department, Aarhus University, DK-8000 Aarhus C. Denmark, September 1991.