Please see my external home page for a contact e-mail address.
I am interested in the use of higher order logic and machine-assisted proof in the verification of computer software. My work involves coding theories of operational semantics using the Isabelle theorem prover.
Arising out of my teaching of CO3095, I have also become interested in ideas of Software Process Improvement. See XML for Structured Requirements, an XML mark-up language supporting Tom Gilb's requirements methodology.
I am a member of the Program Analysis and Construction group at Leicester.
I studied for my Ph.D. at the University of Edinburgh in the Laboratory for the Foundations of Computer Science under the supervision of Professor Mike Fourman and Dr John Power. My thesis on `First Order Linear Logic and Symmetric Monoidal Closed Categories' is available in gzipped PostScript (.ps.gz) and gzipped DVI (.dvi.gz).