Efficient Unification and Backtracking in a Portable, C-based Lisp, R. S. Boyer, W. Schelter. MCC Technical Report AI-102-87, 1987.
On Adding Some Theorem Proving Techniques to Lisp, R. S. Boyer, M. Ballantyne and V. Lifschitz. MCC Technical Report ACA-AI-271-87-Q, 1987.
R. S. Boyer, Rewrite Rule Compilation, MCC Technical Report AI-194-86-P, 1985.
A Prototype Theorem-Prover for a Higher-Order Functional Language, R. S. Boyer, M. Kaufmann, Burroughs Austin Research Center, Technical Report ARC 84-17, 1984.
On the Feasibility of Mechanically Verifying SASL Programs, R. S. Boyer, M. Kaufmann, Burroughs Austin Research Center, Technical Report ARC 84-16, 1984.
The Mechanical Verification of a FORTRAN Square Root Program, R. S. Boyer, J S. Moore. Technical Report, Computer Science Laboratory Report, SRI International, 1981.
A Theorem-Prover for Recursive Functions: A User's Manual, R. S. Boyer, J S. Moore. Technical Report CSL-91, Computer Science Laboratory, SRI International, 1979.
A Provably Secure Operating System: The System, Its Applications, and Proofs, R. S. Boyer, P. G. Neumann, et al. Technical Report CSL-116, Computer Science Laboratory, SRI International, 1977.
Report on the Language Gypsy, Version 2.0. R. M. Cohen, D. I. Good, Lawrence Hunter, and Charles Hoch. Technical Report ICSCA-CMP-10, Institute for Computer Science and Computer Applications, The University of Texas at Austin, May,1978.
Program Design System. R. M. Cohen, Mark Moriconi, Wilhelm Burger, and Mabry Tyson, in Constructing Verifiable and Secure Communications Processing Systems, edited by D. I. Good. Technical Report ICSCA-CMP-6, Institute for Computer Science and Computer Appli- cations, The University of Texas at Austin, January 1977.
R. M. Cohen, Program Design System (Version 4.2) User's Manual. Certifiable Mini- computer Project, Department of Computer Sciences, The University of Texas at Austin, October 1975.
(D. I. Good, R.M. Cohen, C.G. Hoch, L.W. Hunter, D.F. Hare) Report on the Language Gypsy: Version 2.0, ICSCA-CMP-10, September, 1978.
(D. I. Good, A.L. Ambler, John Howard) Program Proof from ICSCA-CMP-6, The University of Texas at Austin, Austin, Texas, 1977.
(D. I. Good, A.L. Ambler) Program Specifications from ICSCA-CMP-6, The University of Texas at Austin, Austin, Texas, 1977.
D. I. Good, (as editor) Constructing Verifiably Reliable and Secure Communications Processing Systems, CMP Final Report, ICSCA-CMP-6, The University of Texas at Austin, Austin, Texas, 1977.
(D. I. Good, A.L. Ambler, W. Burger) Report on the Language Gypsy. CMP Technical Report, ICSCA-CMP-1, The University of Texas at Austin, Austin, Texas, August, 1976.
(D. I. Good, R.L. London, W.W. Bledsoe) An Interactive Program Verification System, ISI-RR-724-22, Information Sciences Institute, Marina del Rey, California, October, 1974.
W. H. Hunt, FM8501: A Verified Microprocessor. Technical Report 47, ICSCA, UT, December 1985.
The Mechanical Verification of a FORTRAN Square Root Program, J S. Moore, R.S. Boyer. CSL Report, SRI International, 1981.
J S. Moore, Text Editing Primitives - The TXDT Package. Technical Report CSL-81-2, Xerox Palo Alto Research Center, 1981.
A Theorem-Prover for Recursive Functions: A User's Manual, J S. Moore, R.S. Boyer. Technical Report CSL-91, Computer Science Laboratory, SRI International, 1979.
J S. Moore, The INTERLISP Virtual Machine Specification. Technical Report CSL-76-5, Xerox Palo Alto Research Center, 1976.
Simmons, R.F. and Smith, M.K., Generating and answering literal English questions from text, Technical Report NL-21, Department of Computer Science, University of Texas, March 1974.
http://dirleton.csres.utexas.edu/staff/publications/noncli.html