R. L. Akers, Gypsy-to-Ada Program Compiler Master's Thesis, University of Texas at Austin, May, 1983, also available as Institute for Computing Science and Computer Applications Technical Report 39, University of Texas at Austin, December, 1983.
W. R. Bevier, A Verified Operating System Kernel Ph.D. dissertation, The University of Texas at Austin, December, 1987. Also appears (minus certain appendices) as CLI Technical Report 11.
R. S. Boyer, Locking: A Restriction of Resolution. Ph. D. Thesis, Mathematics Department, University of Texas, Austin, 1971.
A. Flatau, A Verified Implementation of an Applicative language with Dynamic Storage Allocation, Ph.D. dissertation, The University of Texas at Austin, December, 1992. Also available (minus certain appendices) from Computational Logic as CLI technical report 83.
A. Flatau, A Pascal to Lisp Translator for the Symbolics 3600 Lisp Machine, Master's Thesis, University of Texas at Austin, August, 1985.
D. I. Good, Toward a Man-Machine System for Proving Program Correctness, Ph.D. Thesis, The University of Wisconsin, Madison, Wisconsin, June, 1970.
J S. Moore, Computational Logic: Structure Sharing and Proof of Program Properties, PhD Thesis, Department of Computational Logic,University of Edinburgh, 1973.
M. K. Smith, Knowledge-based Contextual Reference Resolution for Text Understanding, PhD Thesis, Department of Computing Science, University of Texas, December, 1981.
W. D. Young, A Verified Code Generator for a Subset of Gypsy, Ph.D. dissertation, The University of Texas at Austin, August, 1988. Also available (minus certain appendices) from Computational Logic as CLI technical report 33.
http://dirleton.csres.utexas.edu/staff/publications/diss.html