I am a third year PhD student 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 formalize 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.

- Wenda Li, Grant Passmore and Lawrence Paulson
**A Complete Decision Procedure for Univariate Polynomial Problems in Isabelle/HOL**[**preprint**]

- Wenda Li and Lawrence Paulson
**A formal proof of Cauchy's residue theorem**In ITP 2016: Seventh International Conference on Interactive Theorem Proving (Springer LNCS 9807) [**preprint**,**slide**] - Wenda Li and Lawrence Paulson
**A modular, efficient formalisation of real algebraic numbers**In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2016). 2016. [**preprint**,**slide**] - Wenda Li
**The Sturm-Tarski Theorem**Archive of Formal Proofs. 2014. - Wenda Li
**The Königsberg Bridge Problem and the Friendship Theorem**Archive of Formal Proofs. 2013.

Computer Laboratory

University of Cambridge

William Gates Building

15 JJ Thomson Avenue

Cambridge CB3 0FD, UK

firstname.surname (at) cl.cam.ac.uk