| Citation | Larry Paulson has made fundamental contributions to computational logic. He invented the idea of a generic theorem prover, one that could be instantiated to different logical systems with shared proof mechanisation infrastructure. Following a ground-breaking theoretical analysis, he implemented his ideas in an interactive theorem prover, Isabelle. This is now one of the -- perhaps the -- most widely used proof assistants, used in diverse ways by many groups worldwide. Researchers at the Technical University of Munich used Isabelle to check parts of the recently announced mechanical proof of the Kepler conjecture. Researchers at NICTA Australia used it for the first formal verification of an operating system (seL4). Paulson himself has made numerous contributions to both the core ideas of theorem proving and to its applications. Examples include his higher-order theory of rewriting and the "sledgehammer" method for combining automatic first order theorem proving with higher-order reasoning; both of these have had enormous influence on interactive theorem proving. His reseach has influenced the design of a whole generation of interactive proof assistants, including HOL4, HOL Light and ProofPower, which are all still in use. Paulson's most widely known application of theorem proving is his inductive method for "black box" symbolic verification of security protocols and its application to the real world Internet protocols TLS and SET that are widely used in electronic commerce. Recently Paulson has pioneered the application of machine learning to theorem proving. In separate recent research, he has developed and implemented new methods for proving assertions about logarithmic, trigonometric and hyperbolic functions. |