*A Computational Logic Handbook*, with J S. Moore. Academic
Press,

London, 1998. Second Edition. xxv+518

*Automated Reasoning: Essays in Honor of Woody Bledsoe*.
(editor).

Kluwer Academic, Dordrecht, The Netherlands, 1991. Picture of Woody.

*A Computational Logic Handbook*, with J S. Moore. Academic
Press,

New York, 1988. xvi+408

*The Correctness Problem in Computer Science* (editor, with J
S. Moore).

Academic Press, London, 1981.

*A Computational Logic*, with J S. Moore.
Academic Press, New York, 1979. xiv+397. Now public domain.
The original Pub source for the book is here.
The translation to TeX and pdf was kindly done by Gary Klimowicz.

Single-Threaded Objects in ACL2, with J Strother Moore, in S. Krishnamurthi and C. R. Ramakrishnan, editors,

Mechanized Formal Reasoning about Programs and Computing Machines, with J Strother Moore, in Robert Veroff, editor,

Automated Proofs of Object Code for a Widely Used Microprocessor, with Yuan Yu,

Woody Bledsoe: His Life and Legacy, with Michael Ballantyne and Larry Hines,

The Boyer-Moore Theorem Prover and Its Interactive Enhancement,

with M. Kaufmann and J S. Moore,

Automated Correctness Proofs of Machine Code Programs for a Commercial Microprocessor, with Yuan Yu, in D. Kapur, editor,

MJRTY - A Fast Majority Vote Algorithm, with J S. Moore, in Robert S. Boyer, editor,

A Biographical Sketch of W. W. Bledsoe, with Anne Boyer, in Robert S. Boyer, editor,

Functional Instantiation in First Order Logic, with D. Goldschlag, M. Kaufmann, and J Moore, in V. Lifschitz (editor),

A Theorem Prover for a Computational Logic, with J S. Moore, keynote address,

The Use of a Formal Simulator to Verify a Simple Real Time Control Program, with M. W. Green and J S. Moore. in W. H. J. Feijen, A. J. M. van Gasteren, D. Gries, and J. Misra, editors,

The Efficient Implementation of Lattice Operations, with H. Ait-Kaci, P. Lincoln, and R. Nasr.

The Addition of Bounded Quantification and Partial Functions to a Computational Logic and Its Theorem Prover, with J S. Moore,

Integrating Decision Procedures into Heuristic Theorem Provers: A Case Study of Linear Arithmetic, with J S. Moore.

Set Theory in First Order Logic: Clauses for Goedel's Axioms, with E. Lusk, W. McCune, R. Overbeek, M. Stickel, and L. Wos,

Program Verification, with J S. Moore.

A Mechanical Proof of the Turing Completeness of PURE LISP, with J S. Moore. In W. W. Bledsoe and D. W. Loveland, editors, Contemporary Mathematics, Volume 29,

Proof-Checking, Theorem-Proving, and Program Verification, with J S. Moore. In W. W. Bledsoe and D. W. Loveland, editors, Contemporary Mathematics, Volume 29,

Proof Checking the RSA Public Key Encryption Algorithm, with J S. Moore.

A Mechanical Proof of the Unsolvability of the Halting Problem, with J S. Moore.

A Verification Condition Generator for FORTRAN, with J S. Moore. In R. S. Boyer and J S. Moore, editors,

Metafunctions: Proving Them Correct and Using Them Efficiently as New Proof Procedures, with J S. Moore. In R. S. Boyer and J S. Moore, editors,

A Lemma Driven Automatic Theorem Prover for Recursive Function Theory, with J S. Moore.

A Fast String Searching Algorithm, with J S. Moore.

Primitive Recursive Program Transformation, with J S. Moore and R. E. Shostak.

SELECT--A Formal System for Testing and Debugging Programs, with K. N. Levitt and B. Elspas.

Proving Theorems about LISP Functions, with J S. Moore.

The Sharing of Structure in Theorem-proving Programs, with J S. Moore. In B. Meltzer and D. Michie, editors,

Computer Proofs of Limit Theorems, with W. W. Bledsoe and W. H. Henneman,

Circuit Specification, Abstraction, and Reverse Engineering, with Warren Hunt, ACL2 Workshop, 2007.

Function Memoization and Unique Object Representation for ACL2 Functions, with Warren Hunt, ACL2 Workshop, 2006.

A Compressed Format for Collections of Phylogenetic Trees and Improved Consensus Performance, with Warren A. Hunt, Jr., and Serita M. Nelesen. In R. Casadio and G. Meyers, editors, 5th Workshop on Algorithmics in Bioinformatics - WABI 2005. Lecture Notes in Bioinformatics, Springer, LNBI 3692.

Foreword, in

Bledsoe memorial resolution. With J. C. Browne, J. Misra, M. Ballantyne, and L. Hines. Faculty Council, University of Texas at Austin, 3 August 1998. Let's Name the Building for Nobel Prize Winner H. J. Muller, op-ed piece, University of Texas student newspaper

Bledsoe funeral oration, October 7, 1995. http://www.cs.utexas.edu/users/boyer/bledsoe-funeral-oration.html

My views on undergraduate education in computer science, September, 1995. http://www.cs.utexas.edu/users/boyer/rigor-iv.pdf.

Comments upon the document "America in the Age of Information," the Strategic Implementation Plan of the Committee on Information and Communications of the National Science and Technology Council, June 27, 1995. ftp://ftp.cs.utexas.edu/pub/boyer/cic.whitepaper

A Few Minor Remarks (on Metafunctions), Proceedings of the Workshop on Correctness and Metatheoretic Extensibility of Automated Reasoning Systems, INRIA Lorraine, Nancy, France, 1994, p. 22.

Metafunctions in Nqthm and Acl2, with Matt Kaufmann and J Moore, Proceedings of the Workshop on Correctness and Metatheoretic Extensibility of Automated Reasoning Systems, INRIA Lorraine, Nancy, France, 1994, pp. 16-18.

A Mechanically Proof-Checked Encyclopedia of Mathematics: Should We Build One? Can We?, Proceedings of the 12th Annual Conference on Automated Deduction, Springer-Verlag Lecture Notes in Computer Science, Number 814, 1994, p. 237.

The preface to

On the Difficulty of Automating Inductive Reasoning, with J Moore, Remarks made at a workshop on inductive reasoning, Sarasota Springs, NY, June, 1992.

A Formal Specification of Some User Mode Instructions for the Motorola 68020, with Yuan Yu, Technical Report TR-92-04, Computer Sciences Department, University of Texas at Austin, Austin, Texas 78712, 1992.

Article in opposition to a multicultural curricular proposal, University of Texas student newspaper

Response, biographical sketch, and photo on the occasion of receipt of the 1991 AMS Current Award for Automatic Theorem Proving,

The Code for a Computational Logic, with J S. Moore, Technical Report 24, Computational Logic, Inc., Austin, Texas, 1988.

Basic Events for a Computational Logic, with J S. Moore, Technical Report Technical Report 25, Computational Logic, Inc., Austin, Texas 1988.

Efficient Unification and Backtracking in a Portable, C-based Lisp, with W. Schelter. MCC Technical Report AI-102-87, 1987.

On Adding Some Theorem Proving Techniques to Lisp, with M. Ballantyne and V. Lifschitz. MCC Technical Report ACA-AI-271-87-Q, 1987.

Rewrite Rule Compilation, MCC Technical Report AI-194-86-P, 1985.

A Prototype Theorem-Prover for a Higher-Order Functional Language, with M. Kaufmann, Burroughs Austin Research Center, Technical Report ARC 84-17, 1984.

On the Feasibility of Mechanically Verifying SASL Programs, with M. Kaufmann, Burroughs Austin Research Center, Technical Report ARC 84-16, 1984.

The Mechanical Verification of a FORTRAN Square Root Program, with J S. Moore. Technical Report, Computer Science Laboratory Report, SRI International, 1981.

A Theorem-Prover for Recursive Functions, with J S. Moore.

The FORTRAN Verification System, with J S. Moore.

Engineering Notes

A Theorem-Prover for Recursive Functions: A User's Manual, with J S. Moore. Technical Report CSL-91, Computer Science Laboratory, SRI International, 1979.

A Provably Secure Operating System: The System, Its Applications, and Proofs, with P. G. Neumann, et al. Technical Report CSL-116, Computer Science Laboratory, SRI International, 1977.

Pretty-print. Technical Report 64, Department of Computational Logic, University of Edinburgh, 1973.

The Sharing of Structure in Resolution Programs, with J S. Moore. Technical Report, Metamathematics Unit, Edinburgh University, 1972.

The 77-Editor, with J S. Moore and D. J. M. Davies. Technical Report 62, Department of Computational Logic, University of Edinburgh, 1973.

Locking: A Restriction of Resolution. Ph. D. Thesis, Mathematics Department, University of Texas, Austin, 1971.