[2][3][7][8][9] Paulson graduated from the California Institute of Technology in 1977,[10] and obtained his PhD in Computer Science from Stanford University in 1981 for research on programming languages and compiler-compilers supervised by John L.

[14] He has worked on the verification of cryptographic protocols using inductive definitions,[15] and he has also formalised the constructible universe of Kurt Gödel.

Recently he has built a new theorem prover, MetiTarski,[6] for real-valued special functions.

[16] Paulson teaches an undergraduate lecture course in the Computer Science Tripos, entitled Logic and Proof[17] which covers automated theorem proving and related methods.

[20]) Paulson was elected a Fellow of the Royal Society (FRS) in 2017,[5] a Fellow of the Association for Computing Machinery in 2008[1] and a Distinguished Affiliated Professor for Logic in Informatics at the Technical University of Munich.[when?