- "Computer-Aided Reasoning: An Approach" (with P. Manolios and J Moore). Kluwer Academic Publishers, June, 2000.
- "Computer-Aided Reasoning: ACL2 Case Studies" (with co-editors P. Manolios and J Moore). Kluwer Academic Publishers, June, 2000.
- (Chapter) ACL2 and Its Applications to Digital System Verification (with J Strother Moore). In: "Design and Verification of Microprocessor Systems for High-Assurance Applications", David S.~Hardin, ed., Springer, 2010, pp. 1--21.
- (Chapter) A Computational Logic for Applicative Common Lisp (with J Moore). In: "A Companion to Philosophical Logic", D. Jacquette (ed), Blackwell Publishers, pp. 724-741, 2002.
- (Chapter) The Quantifier "There Exist Uncountably Many" and Some of Its Relatives, in: Model-Theoretic Logics (J. Barwise and S. Feferman, editors), Springer-Verlag, 1985, pp. 123-176.
UTCS Research Areas: