BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Australia
1 × Canada
1 × Denmark
1 × France
1 × Ireland
1 × Poland
1 × Portugal
2 × Italy
3 × Germany
3 × USA
Collaborated with:
∅ J.E.Martina J.Meng J.D.Fleuriot G.Bella T.Nipkow J.C.Blanchette S.Böhme C.Benzmüller F.Theiss A.Fietzke R.Narayanan B.Akbarpour M.H.Zaki S.Tahar
Talks about:
theorem (4) induct (3) use (3) protocol (2) isabell (2) prover (2) method (2) secur (2) prove (2) proof (2)

Person: Lawrence C. Paulson

DBLP DBLP: Paulson:Lawrence_C=

Contributed to:

CADE 20152015
SAC 20132013
CADE 20112011
DATE 20102010
IJCAR 20082008
IJCAR 20042004
CADE 20022002
IJCAR 20012001
LICS 19991999
CADE 19981998
CAV 19981998
CADE 19941994
CADE 19921992
CADE 19881988
POPL 19821982

Wrote 15 papers:

CADE-2015-Paulson #automaton #finite #formal method #set #using
A Formalisation of Finite Automata Using Hereditarily Finite Sets (LCP), pp. 231–245.
SAC-2013-MartinaP #induction #multi #protocol #security #using #verification
Verifying multicast-based security protocols using the inductive method (JEM, LCP), pp. 1824–1829.
CADE-2011-BlanchetteBP #smt
Extending Sledgehammer with SMT Solvers (JCB, SB, LCP), pp. 116–130.
DATE-2010-NarayananAZTP #process #verification
Formal verification of analog circuits in the presence of noise and process variation (RN, BA, MHZ, ST, LCP), pp. 1309–1312.
IJCAR-2008-BenzmullerPTF #automation #higher-order #logic #named #proving #theorem proving
LEO-II — A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (CB, LCP, FT, AF), pp. 162–170.
IJCAR-2004-MengP #interactive #proving #using
Experiments on Supporting Interactive Proof Using Resolution (JM, LCP), pp. 372–384.
CADE-2002-Paulson #case study #reasoning #theorem
The Reflection Theorem: A Study in Meta-theoretic Reasoning (LCP), pp. 377–391.
IJCAR-2001-Paulson #proving #set
SET Cardholder Registration: The Secrecy Proofs (LCP), pp. 5–12.
LICS-1999-Paulson #protocol #proving #security
Proving Security Protocols Correct (LCP), pp. 370–381.
CADE-1998-FleuriotP #analysis #geometry #proving #standard #theorem proving
A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton’s Principia (JDF, LCP), pp. 3–16.
CAV-1998-BellaP #induction
Mechanising BAN Kerberos by the Inductive Method (GB, LCP), pp. 416–427.
CADE-1994-Paulson #approach #implementation #induction
A Fixedpoint Approach to Implementing (Co)Inductive Definitions (LCP), pp. 148–161.
CADE-1992-NipkowP
Isabelle-91 (TN, LCP), pp. 673–676.
CADE-1988-Paulson #named #proving #theorem proving
Isabelle: The Next Seven Hundred Theorem Provers (LCP), pp. 772–773.
POPL-1982-Paulson #compilation #generative #semantics
A Semantics-Directed Compiler Generator (LCP), pp. 224–233.
Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.