I am a research associate 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.