Wenda Li

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.

Draft

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

Journal and conference publications

• 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]

Archive of Formal Proofs

• Angeliki Koutsoukou Argyraki and Wenda Li Irrational Rapidly Convergent Series Ar­chive of For­mal Proofs. 2018.
• Wenda Li Count the Number of Complex Roots Ar­chive of For­mal Proofs. 2017.
• Wenda Li Evaluate Winding Numbers through Cauchy Indices Ar­chive of For­mal Proofs. 2017.
• Wenda Li The Sturm-Tarski Theorem Ar­chive of For­mal Proofs. 2014.
• Wenda Li The Königsberg Bridge Problem and the Friendship Theorem Ar­chive of For­mal Proofs. 2013.

Contact

Computer Laboratory
University of Cambridge
William Gates Building
15 JJ Thomson Avenue
Cambridge CB3 0FD, UK
wl302 (at) cam.ac.uk