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 decision procedures within Isabelle/HOL to prove polynomial problems automatically.


  • Wenda Li and Lawrence Paulson Evaluating Winding Numbers through Cauchy Indices in Isabelle/HOL. [pdf]
  • Journal and conference publications

    Archive of Formal Proofs


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