Professor Larry Paulson
Director of Studies for Computer Science
Professor of Computational Logic
t: (01223) 334623
Departmental website: http://www.cl.cam.ac.uk/~lp15/
What is your subject and specific area of study?
I came to computer science with a background in mathematics and logic. At Caltech I had the privilege of meeting N. G. de Bruijn, who had distinguished himself in several branches of mathematics and gone on to do pioneering work in the formalisation of mathematical proofs by computer. I have devoted most of my research career to this area, though others have pursued de Bruijn’s particular way of doing it. The main application of automated proof is to verify the correctness of computer hardware and software; as we all know, computers are not reliable and the majority of their faults lie not in manufacturing flaws but in logical design errors. Such errors could, in principle, be identified using mathematical techniques. My best-known work concerns the verification of security protocols, which all Internet users come into contact with when they visit secure websites. I have investigated the SSL protocol, which is running when your web browser displays the padlock symbol.
What makes Clare College such a good place to study your subject?
Clare is one of the few colleges where the Director of Studies in computer science is a professor engaged in active research. The University of Cambridge Computer Laboratory is probably the world’s oldest computer science department. It built one of the world’s first digital computers. It still leads hardware and systems, while also having strong research groups in security, theory, artificial intelligence and other subjects. Computer science at Cambridge is an entirely different subject from ICT. Our course offerings should appeal to anybody who loves mathematics, electronics or engineering. Our graduates are highly sought after: our most recent annual recruitment fair had nearly 50 firms advertising their employment options.
Main Publications:
Recent Books:
Isabelle/HOL: A Proof Assistant for Higher-Order Logic (with T Nipkow and M Wenzel)
(Springer LNCS 2283, 2002)
ML for the Working Programmer. Second edition
(Cambridge University Press, 1996)
Recent Publications:
MetiTarski: An Automatic Prover for the Elementary Functions, Akbarpour, B; Paulson, LC; in Intelligent Computer Mathematics, S Autexier et al (eds), 217-231
(Springer LNCS 5144, 2008)
Translating higher-order problems to first-order clauses, Meng, J; Paulson, LC, Journal of Automated Reasoning, 40 (1), 35-60 (2008)
Verifying the SET Purchase Protocols, Bella, G; Massacci, F; Paulson, LC, Journal of Automated Reasoning, 36, 5–37 (2006)
The relative consistency of the axiom of choice mechanized using Isabelle/ZF, Paulson, LC, LMS J. Computation and Mathematics, 6, 198–248 (2003)