I am a PhD candidate in the Programming, Logic, and Semantics Group at the Computer Laboratory of the University of Cambridge, under the supervision of Prof. Lawrence C. Paulson. My interest is to formalise mathematics (in an interective theorem prover) that can lead to formal verification of software systems. Currenctly, I am building verified procedures in computer algebra using Isabelle/HOL to reason about nonlinear arithmetic.
Computer Laboratory
University of Cambridge
William Gates Building
15 JJ Thomson Avenue
Cambridge CB3 0FD, UK
wl302 (at) cam.ac.uk