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.

- Wenda Li and Lawrence Paulson
**Evaluating Winding Numbers and Counting Complex Roots through Cauchy Indices in Isabelle/HOL.**[**pdf**]

- Wenda Li, Grant Passmore and Lawrence Paulson
**Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL**Journal of Automated Reasoning, 2017. [**pdf**] - Wenda Li and Lawrence Paulson
**A formal proof of Cauchy's residue theorem**Proceedings of the 7th International Conference on Interactive Theorem Proving, ITP 2016.[**pdf**,**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.[**pdf**,**slide**]

- Wenda Li
**Count the Number of Complex Roots**Archive of Formal Proofs. 2017. - Wenda Li
**Evaluate Winding Numbers through Cauchy Indices**Archive of Formal Proofs. 2017. - 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

wl302 (at) cam.ac.uk