Lawrence C Paulson

Lawrence C. Paulson is Professor of Computational Logic in Computer Laboratory at the University of Cambridge . His research concerns automated theorem proving and its applications: development of Isabelle , with emphasis on automation ; MetiTarski , an automatic prover for the elementary functions; formalising mathematics , including Gödel's incompeteness theorems and constructible universe ; and proving the correctness of security protocols ;