Lawrence C. Paulson

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

Bayesian Optimisation for Premise Selection in Automated Theorem Proving (Student Abstract).

[BibT_eX]

[DOI]

Proceedings of the Thirty-Fourth AAAI Conference on Artificial Intelligence, 2020

2019

Using Machine Learning to Improve Cylindrical Algebraic Decomposition.

[BibT_eX]

[DOI]

Math. Comput. Sci., 2019

Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL.

[BibT_eX]

[DOI]

Grant Olney Passmore

J. Autom. Reason., 2019

From LCF to Isabelle/HOL.

[BibT_eX]

[DOI]

Makarius Wenzel

Formal Aspects Comput., 2019

Bayesian Optimisation with Gaussian Processes for Premise Selection.

[BibT_eX]

[DOI]

CoRR, 2019

Zermelo Fraenkel Set Theory in Higher-Order Logic.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2019

Fourier Series.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2019

Bayesian Optimisation for Heuristic Configuration in Automated Theorem Proving.

[BibT_eX]

[DOI]

Proceedings of the Vampire 2018 and Vampire 2019. The 5th and 6th Vampire Workshops, 2019

Counting polynomial roots in isabelle/hol: a formal proof of the budan-fourier theorem.

[BibT_eX]

[DOI]

Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019

2018

Introduction to Milestones in Interactive Theorem Proving.

[BibT_eX]

[DOI]

Jeremy Avigad

J. Autom. Reason., 2018

Michael John Caldwell Gordon (FRS 1994), 28 February 1948 - 22 August 2017.

[BibT_eX]

[DOI]

CoRR, 2018

Using Machine Learning to Improve Cylindrical Algebraic Decomposition.

[BibT_eX]

[DOI]

CoRR, 2018

Formalising Mathematics In Simple Type Theory.

[BibT_eX]

[DOI]

CoRR, 2018

Quaternions.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2018

The Prime Number Theorem.

[BibT_eX]

[DOI]

Manuel Eberl

Arch. Formal Proofs, 2018

An Isabelle/HOL formalisation of Green's Theorem.

[BibT_eX]

[DOI]

Mohammad Abdulaziz

Arch. Formal Proofs, 2018

2017

Computational Logic: Its Origins and Applications.

[BibT_eX]

[DOI]

CoRR, 2017

Porting the HOL light analysis library: some lessons (invited talk).

[BibT_eX]

[DOI]

Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017

2016

Hammering towards QED.

[BibT_eX]

[DOI]

Cezary Kaliszyk

Josef Urban

J. Formaliz. Reason., 2016

The Cartan Fixed Point Theorems.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2016

Source Coding Theorem.

[BibT_eX]

[DOI]

Quentin Hibon

Arch. Formal Proofs, 2016

Using Machine Learning to Decide When to Precondition Cylindrical Algebraic Decomposition with Groebner Bases.

[BibT_eX]

[DOI]

Proceedings of the 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2016

A Formal Proof of Cauchy's Residue Theorem.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - 7th International Conference, 2016

A modular, efficient formalisation of real algebraic numbers.

[BibT_eX]

[DOI]

Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 2016

2015

A Mechanised Proof of Gödel's Incompleteness Theorems Using Nominal Isabelle.

[BibT_eX]

[DOI]

J. Autom. Reason., 2015

The Higher-Order Prover Leo-II.

[BibT_eX]

[DOI]

J. Autom. Reason., 2015

Verifying multicast-based security protocols using the inductive method.

[BibT_eX]

[DOI]

Jean Everson Martina

Int. J. Inf. Sec., 2015

A Complete Decision Procedure for Univariate Polynomial Problems in Isabelle/HOL.

[BibT_eX]

[DOI]

Grant Olney Passmore

CoRR, 2015

Finite Automata in Hereditarily Finite Set Theory.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2015

Proofs and Reconstructions.

[BibT_eX]

[DOI]

Nik Sultana

Christoph Benzmüller

Proceedings of the Frontiers of Combining Systems - 10th International Symposium, 2015

A Formalisation of Finite Automata Using Hereditarily Finite Sets.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-25, 2015

2014

A Machine-Assisted Proof of Gödel's Incompleteness theorems for the Theory of Hereditarily Finite Sets.

[BibT_eX]

[DOI]

Rev. Symb. Log., 2014

Machine Learning for First-Order Theorem Proving - Learning to Select a Good Heuristic.

[BibT_eX]

[DOI]

James P. Bridge

Sean B. Holden

J. Autom. Reason., 2014

A comparison of three heuristics to choose the variable ordering for CAD.

[BibT_eX]

[DOI]

CoRR, 2014

A Comparison of Three Heuristics to Choose the Variable Ordering for Cylindrical Algebraic Decomposition.

[BibT_eX]

[DOI]

ACM Commun. Comput. Algebra, 2014

Real-Valued Special Functions: Upper and Lower Bounds.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2014

Automated theorem proving for special functions: the next phase.

[BibT_eX]

[DOI]

Proceedings of the Symbolic-Numeric Computation 2014, 2014

Verifying Hybrid Systems Involving Transcendental Functions.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods - 6th International Symposium, NFM 2014, Houston, TX, USA, April 29, 2014

Applying Machine Learning to the Problem of Choosing a Heuristic to Select the Variable Ordering for Cylindrical Algebraic Decomposition.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics - International Conference, 2014

2013

First-order theorem proving.

[BibT_eX]

[DOI]

James P. Bridge

Sean B. Holden

Dataset, April, 2013

Quantified Multimodal Logics in Simple Type Theory.

[BibT_eX]

[DOI]

Christoph Benzmüller

Logica Universalis, 2013

Case Splitting in an Automatic Theorem Prover for Real-Valued Special Functions.

[BibT_eX]

[DOI]

James P. Bridge

J. Autom. Reason., 2013

Extending Sledgehammer with SMT Solvers.

[BibT_eX]

[DOI]

Sascha Böhme

J. Autom. Reason., 2013

LEO-II and Satallax on the Sledgehammer test bench.

[BibT_eX]

[DOI]

Nik Sultana

J. Appl. Log., 2013

The Hereditarily Finite Sets.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2013

Gödel's Incompleteness Theorems.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2013

MetiTarski's Menagerie of Cooperating Systems.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems, 2013

2012

Proving the Impossibility of Trisecting an Angle and Doubling the Cube.

[BibT_eX]

[DOI]

Ralph Romanos

Arch. Formal Proofs, 2012

MetiTarski: Past and Future.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

Real Algebraic Strategies for MetiTarski Proofs.

[BibT_eX]

[DOI]

Grant Olney Passmore

Leonardo Mendonça de Moura

Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2012

2010

Functional Programming in ML.

[BibT_eX]

[DOI]

Proceedings of the Encyclopedia of Software Engineering, 2010

MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions.

[BibT_eX]

[DOI]

J. Autom. Reason., 2010

Multimodal and intuitionistic logics in simple type theory.

[BibT_eX]

[DOI]

Christoph Benzmüller

Log. J. IGPL, 2010

Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers.

[BibT_eX]

[DOI]

Proceedings of the 8th International Workshop on the Implementation of Logics, 2010

Formal verification of analog circuits in the presence of noise and process variation.

[BibT_eX]

[DOI]

Proceedings of the Design, Automation and Test in Europe, 2010

Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers.

[BibT_eX]

[DOI]

Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning, 2010

2009

Lightweight relevance filtering for machine-generated resolution problems.

[BibT_eX]

[DOI]

J. Appl. Log., 2009

Applications of MetiTarski in the Verification of Control and Hybrid Systems.

[BibT_eX]

[DOI]

Proceedings of the Hybrid Systems: Computation and Control, 12th International Conference, 2009

Formal verification of analog designs using MetiTarski.

[BibT_eX]

[DOI]

Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, 2009

2008

Translating Higher-Order Clauses to First-Order Clauses.

[BibT_eX]

[DOI]

J. Autom. Reason., 2008

Fun With Tilings.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2008

The Isabelle Framework.

[BibT_eX]

[DOI]

Makarius Wenzel

Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008

LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description).

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

MetiTarski: An Automatic Prover for the Elementary Functions.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics, 9th International Conference, 2008

2007

Preface.

[BibT_eX]

[DOI]

Bernhard Beckert

J. Autom. Reason., 2007

Source-Level Proof Reconstruction for Interactive Theorem Proving.

[BibT_eX]

[DOI]

Kong Woei Susanto

Proceedings of the Theorem Proving in Higher Order Logics, 20th International Conference, 2007

Extending a Resolution Prover for Inequalities on Elementary Functions.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2007

A Termination Checker for Isabelle Hoare Logic.

[BibT_eX]

[DOI]

Gerwin Klein

Proceedings of 4th International Verification Workshop in connection with CADE-21, 2007

2006

Defining functions on equivalence classes.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2006

Accountability protocols: Formalized and verified.

[BibT_eX]

[DOI]

ACM Trans. Inf. Syst. Secur., 2006

Verifying the SET Purchase Protocols.

[BibT_eX]

[DOI]

J. Autom. Reason., 2006

Erratum to "Automation for interactive proof: First prototype" [Inform. and Comput. 204(2006) 1575-1596].

[BibT_eX]

[DOI]

Claire Quigley

Inf. Comput., 2006

Automation for interactive proof: First prototype.

[BibT_eX]

[DOI]

Claire Quigley

Inf. Comput., 2006

Isabelle/Isar.

[BibT_eX]

[DOI]

Markus Wenzel

Proceedings of the Seventeen Provers of the World, Foreword by Dana S. Scott, 2006

2005

An overview of the verification of SET.

[BibT_eX]

[DOI]

Int. J. Inf. Sec., 2005

Mechanizing compositional reasoning for concurrent systems: some lessons.

[BibT_eX]

[DOI]

Sidi O. Ehmety

Formal Aspects Comput., 2005

Proof Pearl: Defining Functions over Finite Sets.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 18th International Conference, 2005

2004

Organizing Numerical Theories Using Axiomatic Type Classes.

[BibT_eX]

[DOI]

J. Autom. Reason., 2004

Experiments on Supporting Interactive Proof Using Resolution.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - Second International Joint Conference, 2004

2003

The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf.

[BibT_eX]

[DOI]

LMS J. Comput. Math., 2003

Verifying the SET registration protocols.

[BibT_eX]

[DOI]

IEEE J. Sel. Areas Commun., 2003

Verifying Second-Level Security Protocols.

[BibT_eX]

[DOI]

Cristiano Longo

Proceedings of the Theorem Proving in Higher Order Logics, 16th International Conference, 2003

Is the Verification Problem for Cryptographic Protocols Solved?.

[BibT_eX]

[DOI]

Cristiano Longo

Proceedings of the Security Protocols, 2003

2002

Analyzing Delegation Properties.

[BibT_eX]

[DOI]

Proceedings of the Security Protocols, 2002

Program Composition in Isabelle/UNITY.

[BibT_eX]

[DOI]

Sidi O. Ehmety

Proceedings of the 16th International Parallel and Distributed Processing Symposium (IPDPS 2002), 2002

Verifying the SET Protocol: Overview.

[BibT_eX]

[DOI]

Proceedings of the Formal Aspects of Security, First International Conference, 2002

The verification of an industrial payment protocol: the SET purchase phase.

[BibT_eX]

[DOI]

Proceedings of the 9th ACM Conference on Computer and Communications Security, 2002

The Reflection Theorem: A Study in Meta-theoretic Reasoning.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2002

Isabelle/HOL - A Proof Assistant for Higher-Order Logic

[BibT_eX]

[DOI]

Markus Wenzel

Lecture Notes in Computer Science 2283, Springer, ISBN: 3-540-43376-7, 2002

2001

Mechanizing a theory of program composition for UNITY.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2001

Relations Between Secrets: Two Formal Analyses of the Yahalom Protocol.

[BibT_eX]

[DOI]

J. Comput. Secur., 2001

A Simple Formalization and Proof for the Mutilated Chess Board.

[BibT_eX]

[DOI]

Log. J. IGPL, 2001

Mechanical Proofs about a Non-repudiation Protocol.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 14th International Conference, 2001

A Proof of Non-repudiation (Transcript of Discussion).

[BibT_eX]

[DOI]

Proceedings of the Security Protocols, 2001

A Proof of Non-repudiation.

[BibT_eX]

[DOI]

Proceedings of the Security Protocols, 2001

SET Cardholder Registration: The Secrecy Proofs.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, First International Joint Conference, 2001

2000

Mechanizing UNITY in Isabelle.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2000

Mechanizing Nonstandard Real Analysis.

[BibT_eX]

[DOI]

Jacques D. Fleuriot

LMS J. Comput. Math., 2000

Making Sense of Specifications: The Formalization of SET (Transcript of Discussion).

[BibT_eX]

[DOI]

Proceedings of the Security Protocols, 2000

Making Sense of Specifications: The Formalization of SET.

[BibT_eX]

[DOI]

Proceedings of the Security Protocols, 2000

Formal Verification of Cardholder Registration in SET.

[BibT_eX]

[DOI]

Proceedings of the Computer Security, 2000

A fixedpoint approach to (co)inductive and (co)datatype definitions.

[BibT_eX]

Proceedings of the Proof, Language, and Interaction, Essays in Honour of Robin Milner, 2000

1999

Should your specification language be typed.

[BibT_eX]

[DOI]

Leslie Lamport

ACM Trans. Program. Lang. Syst., 1999

Inductive Analysis of the Internet Protocol TLS.

[BibT_eX]

[DOI]

ACM Trans. Inf. Syst. Secur., 1999

Final coalgebras as greatest fixed points in ZF set theory.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 1999

A Generic Tableau Prover and its Integration with Isabelle.

[BibT_eX]

[DOI]

J. Univers. Comput. Sci., 1999

A Formal Proof of Sylow's Theorem.

[BibT_eX]

[DOI]

Florian Kammüller

J. Autom. Reason., 1999

A Pragmatic Approach to Extending Provers by Computer Algebra - with Applications to Coding Theory.

[BibT_eX]

[DOI]

Clemens Ballarin

Fundam. Informaticae, 1999

Locales - A Sectioning Concept for Isabelle.

[BibT_eX]

[DOI]

Florian Kammüller

Markus Wenzel

Proceedings of the Theorem Proving in Higher Order Logics, 12th International Conference, 1999

Relatios Between Secrets: The Yahalom Protocol.

[BibT_eX]

[DOI]

Proceedings of the Security Protocols, 1999

Proving Security Protocols Correct.

[BibT_eX]

[DOI]

Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, 1999

1998

The Inductive Approach to Verifying Cryptographic Protocols.

[BibT_eX]

[DOI]

J. Comput. Secur., 1998

Inductive Analysis of the Internet Protocol TLS (Transcript of Discussion).

[BibT_eX]

[DOI]

Proceedings of the Security Protocols, 1998

Inductive Analysis of the Internet Protocol TLS (Position Paper).

[BibT_eX]

[DOI]

Proceedings of the Security Protocols, 1998

Kerberos Version 4: Inductive Analysis of the Secrecy Goals.

[BibT_eX]

[DOI]

Proceedings of the Computer Security, 1998

Mechanising BAN Kerberos by the Inductive Method.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 10th International Conference, 1998

A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton's Principia.

[BibT_eX]

[DOI]

Jacques D. Fleuriot

Proceedings of the Automated Deduction, 1998

Reasoning About Coding Theory: The Benefits We Get from Computer Algebra.

[BibT_eX]

[DOI]

Clemens Ballarin

Proceedings of the Artificial Intelligence and Symbolic Computation, 1998

Proving Newton's Propositio Kepleriana Using Geometry and Nonstandard Analysis in Isabelle.

[BibT_eX]

[DOI]

Jacques D. Fleuriot

Proceedings of the Automated Deduction in Geometry, 1998

1997

Mechanizing Coinduction and Corecursion in Higher-Order Logic.

[BibT_eX]

[DOI]

J. Log. Comput., 1997

Generic Automatic Proof Tools

[BibT_eX]

[DOI]

CoRR, 1997

Mechanized proofs for a recursive authentication protocol.

[BibT_eX]

[DOI]

Proceedings of the 10th Computer Security Foundations Workshop (CSFW '97), 1997

Proving Properties of Security Protocols by Induction.

[BibT_eX]

[DOI]

Proceedings of the 10th Computer Security Foundations Workshop (CSFW '97), 1997

1996

Mechanizing Set Theory.

[BibT_eX]

[DOI]

Krzysztof Grabczewski

J. Autom. Reason., 1996

Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of Choice.

[BibT_eX]

[DOI]

Krzysztof Grabczewski

CoRR, 1996

ML for the working programmer (2. ed.).

[BibT_eX]

Cambridge University Press, ISBN: 978-0-521-57050-3, 1996

1995

Set Theory for Verification. II: Induction and Recursion.

[BibT_eX]

[DOI]

J. Autom. Reason., 1995

1994

A Concrete Final Coalgebra Theorem for ZF Set Theory.

[BibT_eX]

[DOI]

Proceedings of the Types for Proofs and Programs, 1994

A Fixedpoint Approach to Implementing (Co)Inductive Definitions.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26, 1994

Isabelle - A Generic Theorem Prover (with a contribution by T. Nipkow)

[BibT_eX]

[DOI]

Lecture Notes in Computer Science 828, Springer, ISBN: 3-540-58244-4, 1994

1993

Set Theory for Verification: I. From Foundations to Functions.

[BibT_eX]

[DOI]

J. Autom. Reason., 1993

Designing a Theorem Prover

[BibT_eX]

[DOI]

CoRR, 1993

Isabelle: The Next 700 Theorem Provers

[BibT_eX]

[DOI]

CoRR, 1993

Proving Termination of Normalization Functions for Conditional Expressions

[BibT_eX]

[DOI]

CoRR, 1993

1992

Isabelle-91.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1992

1991

ML for the working programmer.

[BibT_eX]

Cambridge University Press, ISBN: 978-0-521-39022-4, 1991

1989

The Foundation of a Generic Theorem Prover.

[BibT_eX]

[DOI]

J. Autom. Reason., 1989

Logic Programming, Functional Programming, and Inductive Definitions.

[BibT_eX]

[DOI]

Andrew W. Smith

Proceedings of the Extensions of Logic Programming, 1989

1988

A formulation of the simple theory of types (for Isabelle).

[BibT_eX]

[DOI]

Proceedings of the COLOG-88, 1988

Isabelle: The Next Seven Hundred Theorem Provers.

[BibT_eX]

[DOI]

Proceedings of the 9th International Conference on Automated Deduction, 1988

1987

Logic and computation - interactive proof with Cambridge LCF.

[BibT_eX]

Cambridge tracts in theoretical computer science 2, Cambridge University Press, ISBN: 978-0-521-34632-0, 1987

1986

Constructing Recursion Operators in Intuitionistic Type Theory.

[BibT_eX]

[DOI]

J. Symb. Comput., 1986

Natural Deduction as Higher-Order Resolution.

[BibT_eX]

[DOI]

J. Log. Program., 1986

Proving Termination of Normalization Functions for Conditional Experessions.

[BibT_eX]

[DOI]

J. Autom. Reason., 1986

1985

Verifying the Unification Algorithm in LCF.

[BibT_eX]

[DOI]

Sci. Comput. Program., 1985

Lessons Learned from LCF: A Survey of Natural Deduction Proofs.

[BibT_eX]

[DOI]

Comput. J., 1985

1984

Deriving Structural Induction in LCF.

[BibT_eX]

[DOI]

Proceedings of the Semantics of Data Types, International Symposium, 1984

1983

A Higher-Order Implementation of Rewriting.

[BibT_eX]

[DOI]

Sci. Comput. Program., 1983

Compiler Generation from Denotational Semantics.

[BibT_eX]

Proceedings of the Method and tools for compiler construction, 1983

1982

A Semantics-Directed Compiler Generator.

[BibT_eX]

[DOI]

Proceedings of the Conference Record of the Ninth Annual ACM Symposium on Principles of Programming Languages, 1982

1981

A compiler generator for semantic grammars.

[BibT_eX]

[DOI]