% !TEX TS-program = xelatex
% NOTE: ~/public_html/Pages/vita.pdf is a symbolic link to the local copy.

\documentclass[a4paper,11pt]{scrartcl}

\usepackage{microtype}
\usepackage{fontspec,lipsum}
\defaultfontfeatures{Ligatures=TeX}

\setromanfont{Garamond Premier Pro}
\setsansfont{Gill Sans}

\pagestyle{empty}
\usepackage{url}

\def\ha#1{\par\goodbreak\vskip1.8ex\noindent{\large\bfseries\scshape#1}\par\nobreak}

%the \leavevmode begins a new paragraph, which starts with an \hbox.
%OLDER VERSION \def\hb#1{\par\leavevmode\llap{\hbox to 4em{\small#1\hfill}}}
\def\hb#1{\par\noindent\setlength{\hangindent}{4em}%
\leavevmode{\hbox to 4em{\small#1\hfill}}}


\sloppy

\begin{document}

\begin{center}
  {\Large\bfseries Lawrence Charles Paulson FRS}\\[1ex]
  Emeritus Professor of Computational Logic, University of Cambridge \\
  Computer Laboratory, 15 JJ Thomson Avenue, Cambridge CB3 0FD\\
  \emph{E-Mail}: \texttt{lp15@cam.ac.uk}
\end{center}

\parindent0pt\parskip0.6ex

\ha{Academic Appointments}

\hb{2024--}\emph{Emeritus Professor of Computational Logic}, Cambridge. Retired from lecturing, but my College roles persist.

\hb{2002--24}\emph{Professor of Computational Logic}, Cambridge.
Lecture courses include \emph{Logic and Proof} and \emph{Interactive Formal Verification}. Numerous committee and administrative roles.
%2016/17: chairman of examiners for the MPhil and Part III

\hb{1987--}\emph{Fellow} and \textit{Director of Studies}, Clare College, Cambridge.  Responsible for admitting and teaching Clare undergraduates in Computer Science.  Served on many College committees.

\hb{1998--02}\emph{Reader in Computational Logic}, Cambridge. Various teaching and administrative duties.

\hb{1993--98}\emph{University Lecturer}, Cambridge. Lectured on the foundations of logic programming, software engineering and the $\lambda$-calculus.  Chaired the Staff-Student Liaison Committee.

\hb{1983--93}\emph{Assistant Director of Research}, Cambridge.
Lectured on LISP, ML, functional programming, polymorphism, etc. Organised the Computer
Laboratory's Open Days.

\hb{1982--83}\emph{Research assistant} on Prof.\ Robin Milner's LCF project, University of Edinburgh. Conceived and implemented many subsystems of the HOL proof assistant.


\ha{Education}

\hb{1977--81}\emph{Stanford University}, Stanford, CA\@.
% My Ph.D. was conferred on 1/4/1982.
PhD, Computer Science.  For thesis, developed a system to produce compilers
from denotational definitions.  Advisor: Prof.\ John Hennessy.

\hb{1973--77}\emph{California Institute of Technology}, Pasadena,
CA\@.  BS, Mathematics.  Graduated first in class.  Studied computing,
logic and set theory; attended Prof.\ N. G. de~Bruijn's {\scshape Automath} lectures.
Won Motorola Project Award for building a 70-chip computer for Conway's Life.


\parindent0pt\parskip0.6ex

\ha{Editorial Positions}

Editor of \emph{J. Automated Reasoning} and member of the Programme Committees of leading conferences (CADE, TPHOLs, IJCAR, etc.) over many years. Founding editor of \emph{LMS J. Computation and Mathematics} (1998--2007). PC Chairman (with Matt Kaufmann) of the inaugural \textit{Interactive Theorem Proving} (ITP) conference,  2010.
Since 2010, a Trustee of the \textit{Conference on Automated Deduction} (CADE). Since 2016, Chairman of the ITP Steering Committee. Served on various committees of the Royal Society.

\ha{Honours / Awards}

2021 Skolem Award for the 2011 CADE paper ``Extending Sledgehammer with SMT Solvers''

2017 Herbrand Award for Distinguished Contributions to Automated Reasoning

2017 Fellow of the Royal Society

2008 ACM Fellow

2006 Distinguished Affiliated Professor, Technical University of Munich

2003 Pilkington Teaching Prize


\ha{Personal}
Born 20 September 1955, Philadelphia, Pennsylvania;  US/UK nationality.

Married, two children from first marriage. Some competence in German, Russian, Spanish.


%\hb{1995--}Programme Committee, \emph{Formal Methods for Parallel Programming}
%(FMPPTA).

%\hb{1990--96}Editorial board, \emph{Automated Reasoning Series} (Kluwer Academic
%Publishers).

%% \hb{83--90}Review Committee for the {\em Catalogue of Artificial
%% Intelligence Techniques} (Springer).

\parindent=20pt\parskip=0pt
\ha{Research Summary} My field is automated theorem proving, which seeks computational methods for proving theorems in formal logic.
In collaboration with Tobias Nipkow of T.\ U.\ Munich, I have developed a
generic theorem prover, Isabelle, which constructs proofs in a variety of logics
through a novel combination of typed $\lambda$-calculus and unification. Much of my work concerns improving the productivity of interactive proof construction by incorporating the techniques of automatic theorem provers.
Isabelle is used in research projects worldwide.
In earlier work (1982--85, jointly with Michael Gordon and G\'erard Huet), I made major contributions to another theorem prover, HOL, which
became hugely influential by 1990.

I have used Isabelle to formalize a substantial part of axiomatic set theory, in particular
G\"odel's celebrated incompleteness theorems and his proof of the relative consistency of the axiom of
choice. I have developed a flexible method for modelling and verifying
cryptographic protocols, which I have applied to real-world
protocols, including TLS (used on secure websites) and SET, a huge
cryptographic protocol suite for electronic commerce. I have recently developed MetiTarski, an automatic theorem prover for real valued special functions ($\sin$, $\cos$, $\ln$, etc.).
I was co-PI for a £1,051,627 project (joint with Edinburgh) that continued to develop and apply MetiTarski.  I recently completed a six-year, €2.4 million project (an ERC Advanced Grant) to investigate the use of Isabelle in mathematics research.

I have served as  Principal Investigator for eleven UK-funded (EPSRC)
grants, and served as a partner in four ESPRIT projects. I served on the
committee that designed Standard ML and wrote a highly successful textbook on it
(now in its 2nd edition, and translated into two other languages).
Since 2003 I have
belonged to the EPSRC Peer Review College, whose task is to evaluate
funding applications.

\ha{Research Students}

My PhD students include David Wolfram (who finished in 1991), Andrew Gordon
(1992), Martin Coen (1992), Michael Hinchey (1999), Florian Kamm\"uller (1999),
Jacques Fleuriot (1999), Clemens Ballarin (1999), Giampaolo Bella (2000),
Michael Bond (2004), Hyun-Jin Choi (2005), Jia Meng (2005), Michael
Compton (2008), Aaron Coble (2009), James Bridge (2010), Jean Martina (2011), Nikolai Sultana (2014),
William Denman (2015), Zongyan Huang (2015), William Sonnex (2016), Wenda Li (2018), 
Chelsea Edmonds (2024), Kawin Worrasangasilpa (2024) and Chaitanya Mangla.
%23 in the list above
Gordon and Fleuriot received CPHC/BCS Distinguished Dissertation awards (in 1994 and 2000);
Wenda Li was one of two ``highly commended runners-up'' in 2020.
%Also, visitors including Natarajan Shankar, Phillippe de Groote,
% Jacob Frost, Dominique Larchey, Ole S. Rasmussen, Krzysztof
%Gr\c{a}bczewski, Bo Zheng, Pierre Chartier, Thomas M. Rasmussen and Gergely Buday.
%other PhD students Mark Tillotson, Clive Tong, Marcus Moore, James Margetson
%... ao 27 PhD students in all
%1997: James Margetson
%2000: Michael Bond, Hyun-Jin Choi
%2002: Jia Meng, Michael Compton
%2005: Aaron Coble
%2006: James Bridge, Jean Martina
%2008: Nik Sultana, Yichi Zhang. (Yichi soon left to start up a company.)
%2010: William Denman
%2011: William Sonnex (graduated 09/2016)
%2012: Zongyan Huang
%2013: Wenda Li
%2017: Worrasangasilpa
%2018: Mangla (transferred from Mateja Jamnik)
%2019: Chelsea Edmonds

%MPhil supervision
%2017: Frieder Simon

%I served as the external PhD examiner for Lincoln Wallen (Edinburgh), Mark Dawson
%(London), Lucas Dixon (Edinburgh) and Alexander Krauss (TUM)
%President of Jury for Thomas Braibant's thesis defense (Grenoble)
%Rebekah Carter (Manchester)
%Daniel K\"uhlwein (Radboud University) [2014]
% Ondřej Kunčar (TU Munich) [2016]
% Jose Divasón Mallagaray (University of Rioja, Spain) [2016]
% Thomas Sibut-Pinote (Inria Saclay/École Polytechnique, Palaiseau) [2017]
% Daniel Matichuk (University of New South Wales) [2018]
% Kristjan Liiva (University of Edinburgh) [Jan 2019]
% Hing Lun Chan (ANU) [2019]
% Damien Rouhling (Univ de Cote d'Azur) [2019]
% Katherine Cordwell
% Asta Halkjær From

%and as the internal examiner for Stewart Wray,
%Tom Melham, Rajeev Gor\'e, Mads Rosendahl, Jim Grundy, Neil Viljoen, John Harrison,
%Donald Syme, Mark Staples,
%Michael Norrish, Jamie Gabbay, Joe Hurd, Susan Pancho, Hasan Amjad, James Reynolds,
%Thomas Tuerk, Ramana Kumar (2015).
%Edward Ayers, Kyndylan Nienhuis (2021)

% Postdocs trained: Andrew W. Smith (1986), Tobias Nipkow (1988?), Thierry Coquand, Phillippe Noel,
% Sara Kalvala, Chris Owens,
% Giampaolo Bella, Sidi Ehmety, Claire Quigley, Kong Woei Susanto, Behzad Akbarpour, Amine Chaieb,
% Christoph Benzmüller, Grant Passmore, James Bridge
% Anthony Bordg, Wenda Li, Angeliki Koutsoukou-Argyraki, Yiannos Stathopoulos

\ha{Professional Memberships} % Alphabetical, please!

Association for Automated Reasoning (AAR),
Association for Computing Machinery (ACM),
London Mathematical Society (LMS),
Royal Society, University and College Union (UCU)

\newpage
\ha{Invited Lectures}

\begin{enumerate}\frenchspacing

\item Compiler generation from denotational semantics.
\emph{In}:  B. Lorho (editor),
\emph{Methods and Tools for Compiler Construction}
(Cambridge, 1984), 219--251.
Notes for an advanced course held at INRIA-Rocquencourt, France in December 1983.

\item Lessons learned from LCF\@.
DDC Workshop on Formal Software Development: Combining Specification Methods,
Nyborg, Denmark (1984).

\item Joint BCS/SERC Workshop on Program Specification and Verification, York (1983)

\item BCS Formal Aspects of Computing Science, London (1984)

\item Specification and Derivation of Programs, Marstrand, Sweden (1985)

\item IEE/BCS Colloquium on Theorem Provers in Theory and Practice, London (1987)

\item Experience with Isabelle: a generic theorem prover.
COLOG-88: International Conf.\ in Computer Logic,
Tallinn, Estonia, USSR (1988).

\item Applications of proof theory to Isabelle.
Proof Theory Summer School, Leeds (1990).

\item Tool support for logics of programs.
\emph{In}: Manfred Broy (editor),
\emph{Mathematical Methods in Program Development
 (Summer School Marktoberdorf 1996)}
(Springer, 1997), 461--498.

\item Strategic principles in the design of Isabelle,
  \emph{In}: Bernhard Gramlich and Frank Pfenning (editors),
  \emph{CADE-15 Workshop on Strategies in Automated Deduction} (1998), 11--17.

\item Security protocols and their correctness.
\emph{Automated Reasoning Workshop 1998.} St. Andrews, Scotland (1998)

\item Proving security protocols correct.
  \emph{IEEE Symposium on Logic in Computer Science.} Trento, Italy (1999).

\item Getting started with Isabelle. EEF Foundations School on Deduction and Theorem Proving. Edinburgh, Scotland
(2000).

\item SET cardholder registration: the secrecy proofs. \emph{In}: Rajeev Gor\'e,
Alexander Leitsch and Tobias Nipkow (editors),
\emph{Automated Reasoning: First International Joint Conference. IJCAR}, Siena,
Italy.  (Springer, 2001), 5--12.

\item Verifying the SET protocol: overview.  \emph{In}: Ali Abdallah, Peter Ryan and Steve Schneider (editors),
\emph{Formal Aspects of Security}, London, England (2002).

\item Formalizing abstract mathematics: issues and progress.
IJCAR Workshop on \emph{Computer-Supported Mathematical Theory Development}.
Cork, Ireland (2004).

\item Computational logic and the quest for greater automation.
Inaugural lecture upon conferment of the title of Distinguished Affiliated Professor, Munich, Germany (2006).

\item Automated assistance for proof assistants.
\emph{Colloquium in Honour of G{\'e}rard Huet}, Paris, France (2007).

\item Automation for interactive proof: techniques, lessons and prospects.
\emph{Tools and Techniques for Verification of System Infrastructure},
Royal Society, London, UK (2008).

\item The relative consistency of the axiom of choice mechanized using Isabelle/ZF\@.
\emph{Computability in Europe 2008} special session on
Formalising Mathematics and Extracting Algorithms from Proofs,
Athens, Greece (2008).

\item Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. \emph{PAAR-2010: Workshop on Practical Aspects of Automated Reasoning.} Edinburgh, Scotland, July 2010. (Talk given by Jasmin Christian Blanchette.)

\item LCF + logical frameworks = Isabelle (25 years later).
\emph{Milner Symposium.}
Edinburgh, Scotland, April 2012.

\item Overcoming intractable complexity in an automatic theorem prover for real-valued functions.
\emph{CCA 2012: Ninth International Conference on Computability and Complexity in Analysis.}
Cambridge, England, June 2012.

\item MetiTarski: past and future. \emph{Interactive Theorem Proving --- ITP 2012}, Princeton, New Jersey (Springer LNCS 7406, 2012), 1--10.

\item Isabelle/HOL tutorial: verifying functional programs and inductively defined sets. \emph{13th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 13).}
Cambridge, England, September 2012.

\item MetiTarski's menagerie of cooperating systems.
Plenary lecture for the FroCoS and Tableaux conferences.
Nancy, France, September 2013.

\item Theorem proving and the real numbers: overview and challenges.
Keynote lecture for \textit{NASA Formal Methods}.
Houston, Texas, April 2014.

\item Automated theorem proving for special functions: the next phase.
Keynote lecture for SNC 2014 (\textit{Symbolic-Numeric Computation}).
Shanghai, China, July 2014.

\item The future of formalised mathematics.
Keynote lecture for EACA 2016 (XV Encuentro de Álgebra Computacional y Aplicaciones). Logroño, Spain, June 2016.

\item Porting the HOL Light analysis library: Some lessons.
Keynote lecture for CPP 2017 (Certified Programs and Proofs). Paris, France, January 2017.

\item Proof assistants: From symbolic logic to real mathematics? ``Jacques Morgenstern'' Colloquium, Inria Sophia-Antipolis, France, May 2017.

\item Proof assistants: From symbolic logic to real mathematics? \textit{Big Proof} programme, Isaac Newton Institute for Mathematical Sciences, Cambridge, UK, July 2017.

\item Proof support for hybrid system analysis.
\emph{Logical Methods for Safety and Security of Software Systems
 (Summer School Marktoberdorf 2017)}.

\item Automatic theorem proving: impressions from the interactive world.
Herbrand Award acceptance speech. \textit{Conference on Automated Deduction (CADE-26).} 
Gothenburg, Sweden, August 2017.

\item A career in research: Mike Gordon and hardware verification.
\textit{Automated Reasoning Workshop}, Cambridge, UK, April 2018.

\item Formalising mathematics in simple type theory.
\textit{Big Proof} programme,  International Centre for Mathematical Sciences, Edinburgh, UK, May 2019.

\item Machine learning and the formalisation of mathematics: research challenges.
Keynote lecture for Conference on \emph{Artificial Intelligence and Theorem Proving} (AITP). Aussois, France (virtually), September 2020.

\item Doing mathematics with simple types: infinitary combinatorics in Isabelle/HOL\@.
Harvard University Centre of Mathematical Sciences and Applications (virtually), March 2021. 

\item Formalising contemporary mathematics in simple type theory. 
Topos Institute Colloquium (virtually), July 2021.

\item Formalised mathematics: obstacles and achievements.
Zhejiang University  (virtually), September 2021.

\item Automated theorem proving: a technology roadmap.
\emph{Huawei Mathematical Theorem Proving Workshop}. Cambridge, UK, April 2022.

\item Formalising Erdős and Larson: ordinal partition theory.
\emph{Leeds Logic Seminar}, University of Leeds, UK, March 2023.

\item Formalising a number theory textbook: lessons learnt.
University of Cambridge \emph{Symposium for Andrew Pitts}, Cambridge, UK, August 2023.

\item Large-scale formal proof for the working mathematician: lessons learnt from ALEXANDRIA\@. Keynote lecture for \emph{Conference on Intelligent Computer Mathematics}, Cambridge, UK, September 2023.

\item Formalising 21st-century mathematics.
London Mathematical Society / Formal Aspects of Computing evening seminar (virtual), January 2024.

\item Formalising advanced mathematics in Isabelle/HOL.
Workshop on \emph{Prospects of Formal Mathematics}, Hausdorff Centre for Mathematics, Bonn, Germany, June 2024 

\item Sledgehammer: a saga.
Invited talk, \emph{Vampire Workshop}, IDMC Nancy, France, June 2024 

\item Computer algebra and the formalisation of new mathematics.
Invited talk, \emph{SC${}^2$ Workshop}, IDMC Nancy, France, June 2024 
\end{enumerate}

\newpage

\input{publications.tex}

\vfill\noindent {\tiny Last updated \today}

%\newpage
%\input{teaching.tex}

\end{document}
