[2]Kapur, Deepak & Subramaniam, Mahadevan; Mechanically
verifying a family of multiplier circuits; (appearing in Proceedings
of Computer Aided Verification, Springer LNCS 1102, Alur and Henzinger [eds],
1996.
[3]Miller, Steve & Srivas, Mandayam; Formal verification of
the AAMP5 microprocessor: A case study in the industrial use of formal
methods; (appearing in Workshop on Industrial-strength Formal Specification
Techniques, Boca Raton, FL, 1995).
[4]Srivas, Mandayam & Bickford, Mark; Moving formal methods
into practice: Verifying the FTTP scoreboard: Phase 1 results"; NASA
CR-189607, May 1992.
[5]Moore, J Strother & Lynch, T. & Kaufmann, Matt; A
mechanically checked proof of the correctness of the AMD5K86 floating
point division algorithm. http://www.cli.com/news/amd.html
[6]Barwise, Jon; Proofs of Computer Correctness; Notices of
the American Mathematical Society, 1990.
[7]Andrews, Peter B.; An Introduction to
Mathematical Logic and Type Theory: To Truth Through Proof;
Academic Press, New York, 1986.
[8]Crow, J & Owre, S & Rushby, John, Shankar,
Natarajan & Srivas, Mandayam; A Tutorial Introduction to PVS
(appearing in Workshop on Industrial-Strength Formal Specification
Techniques,Boca Raton, FL, 1995.
[9]McMillan, K. L.; Symbolic Model Checking: An Approach to
the State Explosion Problem; Kluwer Academic Publishers, 1993.
[10]Bryant, Randy E; Graph-based algorithms for boolean
function manipulations; IEEE Transactions on Computers; C-35, 8.
[11]Gordon, Michael J. C. & Melham, Thomas F.; Introduction
to HOL; Cambridge University Press, Cambridge, UK, 1993.
[12]Paulson, Larry C; Isabelle; Springer LNCS
828, 1994.
[13] Cornes, C et al; The Coq Proof Assistant Reference
Manual, Version 5.10. Rapport technique RT-0177, INRIA, France, 1995.
[14]Boyer, R. S. & Moore, J. S.; A Computational Logic
Handbook. Academic Press, New York, 1988.
[15](An actual footnote on the often discussed but rarely cited
"Hilbert Program"--credit John Harrison)
[16]Craigen, Dan & Gerhart, S & Ralston, T; Formal
methods reality check: Industrial Usage; IEEE Transactions on Software
Engineering; V21, #2 (Feb) 1995.
[17] Kumar, Ramayya & Kropf, Thomas & Schneider, Klaus;
Integrating a First-Order Automatic Prover in the HOL Environment;
(appearing in Proceedings of the 1991 International Workshop on the
HOL Proving System and Its Applications; IEEE Press, Los Alamitos, CA).
[18] Idea credited without citation to Robin Milner in [11]
[19]Milner, Robin & Tofte, Mads & Harper, R.; The Definition
of Standard ML; The MIT Press, Cambridge MA, 1990.
[20]Milner, Robin & Tofte, Mads; Commentary on
Standard ML; The MIT Press, Cambridge MA, 1991.
[21]VanInwegen, Myra; The Machine-Assisted Proof of Programming Language Properties; University of Pennsylvania, PhD Dissertation, August 1996.
[22]Leroy, Xavier; The Caml Light system, documentation and
user's guide, Release 0.73; http://pauillac.inria.fr/caml/man-caml/index.html;
January, 1997.
[23]Appel, Andrew W & Tarditi, David R; ML-Yacc
User's Manual, Version 2.1 (appearing in SML Distribution, Version
0.93 ftp://ftp.research.bell-labs.com/dist/smlnj/release/93/).
[24]Harrison, John;
b) HOL Light--A Tutorial Introduction; (appearing in Proceedings of the First International Conference on Formal Methods in Computer-Aided Design;LNCS 1166; Srivas & Camilleri [eds], 1996).
[25]Boulton, Richard; Efficiency in a Fully-Expansive
Theorem Prover; PhD Thesis; University of Cambridge Computer Lab,
TR-337, 1993.
[26]Melham, Thomas F; HOL88: Version 12 overview;
(appearing in Proceedings of the Third HOL Users Meeting; DAIMI PB-340;
Aarhus University, December 1990).
[27]Slind, Konrad; Details of a new HOL implementation in SML;
(appearing in Proceedings of the Third HOL Users Meeting; DAIMI PB-340;
Aarhus University, December 1990). [The paper describes the original version of the system and is now outdated. Get the system (HOL90.9) at:
http://www.cl.cam.ac.uk/Research/HVG/FTP/FTP.html]
[28]Archer, Myla & Joyce, Jeffrey & Levitt, Karl &
Windley, Philip; Introduction; (appearing in Proceedings of the 1991
International Workshop on the HOL Proving System and Its
Applications; IEEE Press, Los Alamitos, CA).
[29]Camilleri, Albert J.; A Hybrid Approach to
Verifying Liveness in a Symmetric Multi-Processor; (appearing in
Theorem Proving in Higher Order Logics, Springer LNCS 1275,
Gunter & Felty [eds], 1997).
[30]Gunter, Elsa L.; Adding Decision Procedures to HOL
'90 Securely; (appearing in Supplementary Proceedings of Theorem
Proving in Higher Order Logics, Gunter & Felty [eds], 1997).
[31]Harrison, John; Verifying the Accuracy of
Polynomial Approximations in HOL; (appearing in Theorem Proving in
Higher Order Logics, Springer LNCS 1275, Gunter & Felty [eds],
1997).
[32]The Contributed Libraries for HOL '88;
(http://www.cl.cam.ac.uk/Research/HVG/FTP/FTP.html)
[33]Smith, Brian Cantwell; "Reflection and Semantics in LISP;
(appearing in 14th ACM Symposium on Principles of Programming Languages,
pg 23-35,1984).
[34]Harrison, John; "Metatheory and Reflection in Theorem Proving: A Survey and Critique"; SRI International Cambridge Research Center,
CRC-053, 15 Feb 1995. (available at http://www.cl.cam.ac.uk/Research/HVG/FTP/FTP.html)
[35]Joyce, Jeffrey J & Seger C.; The HOL-Voss system: Model-checking inside a general purpose theorem-prover.; (appearing in Proceedings of the 1993 International Workshop on the HOL theorem proving system and its applications; Springer LNCS 780, 1993.)
[36]Aagaard, Mark & Leeser, Miriam E.; Verifying a Logic Synthesis Tool in Nuprl: A Case Study in Software Verification; (appearing in Proceedings of the 4th Internationall Workshop on Computer-Aided Verification;
Springer LCNS 663, 1993.)
[37]Allen, S & Constable, Robert & Howe, Douglas & Aitken, W.;
The Semantics of Reflected Proof; (appearing in Proceedings fo the Fifth Annual Symposium on Logic in Computer Science; IEEE Computer Society Press,
Los Alamitos, CA, 1990).
Kreisel, G; Hilbert's Programme; Dialectica, V 12, 346-372. (Revised version in Benaceeraf P. & Putnam, H., Philosophy of Mathematics: Selected Readings, 2nd Edition, Cambridge University Press, 1983.)
a) HOL Done Right, unpublished draft, (http://www.cl.cam.ac.uk/users/jrh/papers/holright.html)