
The Inductive Approach to Verifying Cryptographic Protocols
Informal arguments that cryptographic protocols are secure can be made r...
read it

A Mechanised Proof of Gödel's Incompleteness Theorems using Nominal Isabelle
An Isabelle/HOL formalisation of Gödel's two incompleteness theorems is ...
read it

The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle/ZF
The proof of the relative consistency of the axiom of choice has been me...
read it

Ackermann's Function in Iterative Form: A Proof Assistant Experiment
Ackermann's function can be expressed using an iterative algorithm, whic...
read it

Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL
We give an overview of our formalizations in the proof assistant Isabell...
read it

Modelling HighLevel Mathematical Reasoning in Mechanised Declarative Proofs
Mathematical proofs can be mechanised using proof assistants to eliminat...
read it

Bayesian Optimisation with Gaussian Processes for Premise Selection
Heuristics in theorem provers are often parameterised. Modern theorem pr...
read it

Defining Functions on Equivalence Classes
A quotient construction defines an abstract type from a concrete type, u...
read it

Inductive Analysis of the Internet Protocol TLS
Internet browsers use security protocols to protect sensitive messages. ...
read it

From LCF to Isabelle/HOL
Interactive theorem provers have developed dramatically over the past fo...
read it

Counting Polynomial Roots in Isabelle/HOL: A Formal Proof of the BudanFourier Theorem
Many problems in computer algebra and numerical analysis can be reduced ...
read it

Michael John Caldwell Gordon (FRS 1994), 28 February 1948 – 22 August 2017
Michael Gordon was a pioneer in the field of interactive theorem proving...
read it

Using Machine Learning to Improve Cylindrical Algebraic Decomposition
Cylindrical Algebraic Decomposition (CAD) is a key tool in computational...
read it

Formalising Mathematics In Simple Type Theory
Despite the considerable interest in new dependent type theories, simple...
read it

Evaluating Winding Numbers and Counting Complex Roots through Cauchy Indices in Isabelle/HOL
In complex analysis, the winding number measures the number of times a p...
read it

Evaluating Winding Numbers through Cauchy Indices in Isabelle/HOL
In complex analysis, the winding number measures the number of times a p...
read it

Computational Logic: Its Origins and Applications
Computational Logic is the use of computers to establish facts in a logi...
read it

Using Machine Learning to Decide When to Precondition Cylindrical Algebraic Decomposition With Groebner Bases
Cylindrical Algebraic Decomposition (CAD) is a key tool in computational...
read it

Quantified Multimodal Logics in Simple Type Theory
We present a straightforward embedding of quantified multimodal logic in...
read it
Lawrence C. Paulson
verfied profile
Distinguished Affiliated Professor for Logic in Informatics at TU München, Professor of Computational Logic at University of Cambridge, Reader in Computational Logic at University of Cambridge from 19982002, University Lecturer at University of Cambridge from 19931998, Assistant Director of Research, University of Cambridge at University of Cambridge from 19831993, Research assistant at University of Edinburgh from 19821983