Curriculum Vitae for Larry Paulson

• Academic Appointments
• Education
• Editorial Positions
• Awards
• On other pages: Research Grants and Invited Lectures and Publications

Academic Appointments

• 2002–present. Professor of Computational Logic, University of Cambridge.
• 1998–2002. Reader in Computational Logic, University of Cambridge
• 1993–1998. University Lecturer, University of Cambridge. Chair of Staff-Student Consultative Committee. Involved with Computer Laboratory publicity and Open Days.
• 1987–present. Fellow, Clare College, Cambridge. Member of Council and Computer Committee. Director of Studies in Computer Science, responsible for individual tution of all Computer Science students in Clare.
• 1983–1993. Assistant Director of Research, University of Cambridge.
• 1982–1983. Research assistant, University of Edinburgh. With G. Huet, rewrote the theorem prover Edinburgh LCF. The resulting `Cambridge LCF' later became the Cambridge HOL system. Used Cambridge LCF to verify a unification function.

Education

• 1977–81. Stanford University, Stanford, CA. PhD, Computer Science. Wrote a system to produce compilers from denotational definitions. Researched program verification. Advisor: John Hennessy.
• 1973–77. California Institute of Technology, Pasadena, CA. BS, Mathematics.

Editorial Positions

• 1997–present. Editorial board, Journal of Automated Reasoning and LMS Journal of Computation and Mathematics
• 1996–present. Programme Committee, Conference on Automated Deduction (CADE)
• 1996–present. Programme Committee, Theorem Proving in Higher Order Logics (TPHOLS)
• 1995–present. Programme Committee. Formal Methods for Parallel Programming (FMPPTA).

Awards

• 2003 Pilkington Teaching Prize (photo)