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 decision procedures within Isabelle/HOL to prove polynomial problems automatically.
University of Cambridge
William Gates Building
15 JJ Thomson Avenue
Cambridge CB3 0FD, UK
firstname.surname (at) cl.cam.ac.uk