Skip to content


Fellows Directory

Lawrence Paulson

Lawrence Paulson

Professor Lawrence Paulson FRS


Elected: 2017





Lawrence Paulson ( is Professor of Computational Logic at the University of Cambridge, where he has held established positions since 1983. He has written nearly 100 refereed conference and journal papers as well as four books. He introduced the popular [Isabelle]( theorem proving environment in 1986, and made contributions to the verification of cryptographic protocols, the formalisation of mathematics, automated theorem proving technology, and other fields. Specific accomplishments include a formal analysis of the ubiquitous TLS protocol, which is used to secure online shopping, and the formal verification of Gödel's second incompleteness theorem.

In 2008, he introduced MetiTarski (, an automatic theorem prover for real-valued functions such as logarithms and exponentials. He has supervised over 20 postgraduate students and numerous postdoctoral researchers. He has the honorary title of Distinguished Affiliated Professor ( from the Technical University of Munich and is an ACM Fellow (

Professional positions

Professor of Computational Logic, Computer Laboratory, University of Cambridge

Interest and expertise

Subject groups

  • Engineering
    • Computer engineering (including software)
  • Other
    • Other interests
  • Computer sciences
    • Computer science (excl engineering aspects)


“Automated theorem proving”, “computer security (foundations of)”, “logic”, “philosophy of mathematics”, “verification”

Was this page useful?
Thank you for your feedback
Thank you for your feedback. Please help us improve this page by taking our short survey.