%% This BibTeX bibliography file was created using BibDesk.
%% http://bibdesk.sourceforge.net/


%% Created for Larry Paulson at 2012-07-18 15:12:20 +0100 


%% Saved with string encoding Western (Windows Latin 1) 


@string{jar = {J. Automated Reasoning}}


@incollection{passmore-real,
	Affiliation = {Computer Laboratory, University of Cambridge, UK},
	Author = {Passmore, Grant and Paulson, Lawrence and de Moura, Leonardo},
	Booktitle = {Intelligent Computer Mathematics},
	Date-Added = {2012-07-18 14:12:14 +0000},
	Date-Modified = {2012-07-18 14:12:14 +0000},
	Doi = {10.1007/978-3-642-31374-5_24},
	Editor = {Jeuring, Johan and Campbell, John and Carette, Jacques and Dos Reis, Gabriel and Sojka, Petr and Wenzel, Makarius and Sorge, Volker},
	Isbn = {978-3-642-31373-8},
	Pages = {358-370},
	Publisher = {Springer},
	Series = {Lecture Notes in Computer Science},
	Title = {Real Algebraic Strategies for MetiTarski Proofs},
	Url = {http://dx.doi.org/10.1007/978-3-642-31374-5_24},
	Volume = {7362},
	Year = {2012},
	Bdsk-Url-1 = {http://dx.doi.org/10.1007/978-3-642-31374-5_24}}

@inproceedings{blanchette-extending,
	Acmid = {2032277},
	Author = {Blanchette, Jasmin Christian and B\"{o}hme, Sascha and Paulson, Lawrence C.},
	Booktitle = {Automated Deduction --- {CADE}-23},
	Date-Added = {2011-12-20 15:23:21 +0000},
	Date-Modified = {2011-12-20 15:23:21 +0000},
	Editor = {Bj{\o}rner, Nikolaj; Sofronie-Stokkermans, Viorica},
	Isbn = {978-3-642-22437-9},
	Numpages = {15},
	Pages = {116-130},
	Publisher = {Springer-Verlag},
	Title = {Extending {Sledgehammer} with {SMT} solvers},
	Url = {http://dl.acm.org/citation.cfm?id=2032266.2032277},
	Year = {2011},
	Bdsk-Url-1 = {http://dl.acm.org/citation.cfm?id=2032266.2032277}}

@inproceedings{narayanan-formal,
	Address = {3001 Leuven, Belgium, Belgium},
	Author = {Narayanan, Rajeev and Akbarpour, Behzad and Zaki, Mohamed H. and Tahar, Sofi\`{e}ne and Paulson, Lawrence C.},
	Booktitle = {DATE '10: Conference on Design, Automation and Test in Europe},
	Date-Added = {2011-05-06 11:25:11 +0100},
	Date-Modified = {2011-05-06 11:25:17 +0100},
	Isbn = {978-3-9810801-6-2},
	Location = {Dresden, Germany},
	Pages = {1309-1312},
	Publisher = {European Design and Automation Association},
	Title = {Formal Verification of Analog Circuits in the Presence of Noise and Process Variation},
	Url = {http://portal.acm.org/citation.cfm?id=1870926.1871240},
	Year = {2010},
	Bdsk-Url-1 = {http://portal.acm.org/citation.cfm?id=1870926.1871240}}

@inproceedings{akbarpour-hscc,
	Author = {Behzad Akbarpour and Lawrence C. Paulson},
	Booktitle = {Hybrid Systems: Computation and Control},
	Date-Added = {2010-02-25 15:08:34 +0000},
	Date-Modified = {2010-02-25 15:08:34 +0000},
	Editor = {Rupak Majumdar and Paulo Tabuada},
	Pages = {1-15},
	Publisher = {Springer},
	Series = {LNCS 5469},
	Title = {Applications of {MetiTarski} in the Verification of Control and Hybrid Systems},
	Year = {2009}}

@inproceedings{denman-analog,
	Author = {William Denman and Behzad Akbarpour and Sofi{\`e}ne Tahar and Mohamed Zaki and Lawrence C. Paulson},
	Booktitle = {Formal Methods in Computer Aided Design},
	Date-Added = {2010-02-25 15:06:21 +0000},
	Date-Modified = {2010-02-25 15:06:21 +0000},
	Doi = {10.1109/FMCAD.2009.5351136},
	Editor = {Armin Biere and Carl Pixley},
	Pages = {93-100},
	Publisher = {IEEE},
	Title = {Formal Verification of Analog Designs using {MetiTarski}},
	Url = {http://dx.doi.org/10.1109/FMCAD.2009.5351136},
	Year = {2009},
	Bdsk-Url-1 = {http://dx.doi.org/10.1109/FMCAD.2009.5351136}}

@article{benzmueller-multimodal,
	Abstract = {We study straightforward embeddings of propositional normal multimodal logic and propositional intuitionistic logic in simple type theory. The correctness of these embeddings is easily shown. We give examples to demonstrate that these embeddings provide an effective framework for computational investigations of various non-classical logics. We report some experiments using the higher-order automated theorem prover LEO-II.
},
	Author = {Benzmueller, Christoph and Paulson, Lawrence C.},
	Date-Added = {2010-02-25 15:04:02 +0000},
	Date-Modified = {2010-02-25 15:04:42 +0000},
	Doi = {10.1093/jigpal/jzp080},
	Eprint = {http://jigpal.oxfordjournals.org/cgi/reprint/jzp080v1.pdf},
	Journal = {Logic Jnl IGPL},
	Pages = {jzp080},
	Title = {Multimodal and Intuitionistic Logics in Simple Type Theory},
	Url = {http://jigpal.oxfordjournals.org/cgi/content/abstract/jzp080v1},
	Year = {2010},
	Bdsk-Url-1 = {http://jigpal.oxfordjournals.org/cgi/content/abstract/jzp080v1},
	Bdsk-Url-2 = {http://dx.doi.org/10.1093/jigpal/jzp080}}

@article{metitarski-jar,
	Abstract = {Many inequalities involving the functions ln, exp, sin, cos, etc., can be proved automatically by MetiTarski: a resolution theorem prover (Metis) modified to call a decision procedure (QEPCAD) for the theory of real closed fields. The decision procedure simplifies clauses by deleting literals that are inconsistent with other algebraic facts, while deleting as redundant clauses that follow algebraically from other clauses. MetiTarski includes special code to simplify arithmetic expressions. },
	Author = {Akbarpour, Behzad and Paulson, Lawrence},
	Date-Added = {2010-02-25 15:02:24 +0000},
	Date-Modified = {2010-02-25 15:02:24 +0000},
	Doi = {10.1007/s10817-009-9149-2},
	Journal = {J. Auto. Reas.},
	Month = mar,
	Number = {3},
	Pages = {175-205},
	Title = {{MetiTarski}: An Automatic Theorem Prover for Real-Valued Special Functions},
	Url = {http://www.springerlink.com/content/k174817683p20v03/?p=d8a4f25391a74d3987218997722458c1&pi=13},
	Volume = {44},
	Year = {2010},
	Bdsk-Url-1 = {http://dx.doi.org/10.1007/978-3-540-85110-3_18}}

@inproceedings{wenzel-isabelle-framework,
	Author = {Makarius Wenzel and Lawrence C. Paulson and Tobias Nipkow},
	Booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} 2008},
	Date-Added = {2009-07-16 12:20:35 +0100},
	Date-Modified = {2009-07-16 12:24:21 +0100},
	Doi = {10.1007/978-3-540-71067-7_7},
	Editor = {Otmane A\"{\i}t Mohamed and C{\'e}sar Mu{\~n}oz and Sofi{\`e}ne Tahar},
	Pages = {33-38},
	Publisher = {Springer},
	Series = {LNCS 5170},
	Title = {The {Isabelle} Framework},
	Url = {http://dx.doi.org/10.1007/978-3-540-71067-7_7},
	Year = {2008},
	Bdsk-Url-1 = {http://dx.doi.org/10.1007/978-3-540-71067-7_7}}

@article{meng-relevance-jal,
	Author = {Jia Meng and Lawrence C. Paulson},
	Date-Added = {2009-03-06 15:50:24 +0000},
	Date-Modified = {2009-03-06 15:54:54 +0000},
	Doi = {10.1016/j.jal.2007.07.004},
	Journal = {Journal of Applied Logic},
	Number = {1},
	Pages = {41-57},
	Title = {Lightweight Relevance Filtering for Machine-Generated Resolution Problems},
	Volume = {7},
	Year = {2009},
	Bdsk-Url-1 = {http://dx.doi.org/10.1016/j.jal.2007.07.004}}

@inproceedings{leo2-description,
	Author = {Christoph Benzm{\"u}ller and Lawrence C. Paulson and Frank Theiss and Arnaud Fietzke},
	Booktitle = {Automated Reasoning --- 4th International Joint Conference, IJCAR 2008},
	Date-Added = {2008-09-02 14:23:27 +0100},
	Date-Modified = {2008-09-02 14:23:27 +0100},
	Doi = {10.1007/978-3-540-71070-7_14},
	Editor = {Armando, Alessandro and Baumgartner, Peter and Dowek, Gilles},
	Publisher = {Springer},
	Series = {LNAI 5195},
	Title = {{LEO-II} - A Cooperative Automatic Theorem Prover for Higher-Order Logic},
	Url = {http://dx.doi.org/10.1007/978-3-540-71070-7_14},
	Year = {2008},
	Bdsk-Url-1 = {http://dx.doi.org/10.1007/978-3-540-71070-7_14}}

@article{akbarpour2008,
	Abstract = {Many inequalities involving the functions ln, exp, sin, cos, etc., can be proved automatically by MetiTarski: a resolution theorem prover (Metis) modified to call a decision procedure (QEPCAD) for the theory of real closed fields. The decision procedure simplifies clauses by deleting literals that are inconsistent with other algebraic facts, while deleting as redundant clauses that follow algebraically from other clauses. MetiTarski includes special code to simplify arithmetic expressions. },
	Author = {Akbarpour, Behzad and Paulson, Lawrence},
	Date-Added = {2008-09-02 13:56:24 +0100},
	Date-Modified = {2008-09-02 13:56:24 +0100},
	Doi = {dx.doi.org/10.1007/978-3-540-85110-3_18},
	Journal = {Intelligent Computer Mathematics},
	Pages = {217-231},
	Title = {MetiTarski: An Automatic Prover for the Elementary Functions},
	Url = {http://dx.doi.org/10.1007/978-3-540-85110-3_18},
	Year = {2008},
	Bdsk-Url-1 = {http://dx.doi.org/10.1007/978-3-540-85110-3_18}}

@proceedings{tphols07,
	Booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} 2007},
	Date-Added = {2008-01-03 11:25:50 +0000},
	Date-Modified = {2008-01-03 11:25:50 +0000},
	Doi = {10.1007/978-3-540-74591-4},
	Editor = {Klaus Schneider and Jens Brandt},
	Publisher = {Springer},
	Series = {LNCS 4732},
	Title = {Theorem Proving in Higher Order Logics: {TPHOLs} 2007},
	Url = {http://www.springerlink.com/content/978-3-540-74590-7/},
	Year = {2007},
	Bdsk-Url-1 = {http://www.springerlink.com/content/978-3-540-74590-7/},
	Bdsk-Url-2 = {http://dx.doi.org/10.1007/978-3-540-74591-4}}

@inproceedings{paulson-susanto,
	Author = {Lawrence C. Paulson and Kong Woei Susanto},
	Crossref = {tphols07},
	Date-Added = {2008-01-03 11:25:23 +0000},
	Date-Modified = {2008-01-03 11:25:47 +0000},
	Pages = {232-245},
	Title = {Source-Level Proof Reconstruction for Interactive Theorem Proving},
	Url = {http://www.cl.cam.ac.uk/~lp15/papers/Automation/reconstruction.pdf},
	Bdsk-Url-1 = {http://www.cl.cam.ac.uk/~lp15/papers/Automation/reconstruction.pdf}}

@inproceedings{meng-termination,
	Address = {Bremen, Germany},
	Author = {Jia Meng and Lawrence C. Paulson and Gerwin Klein},
	Booktitle = {4th International Verification Workshop - VERIFY'07},
	Date-Added = {2008-01-03 11:24:38 +0000},
	Date-Modified = {2008-01-03 11:24:38 +0000},
	Editor = {Bernhard Beckert},
	Issn = {1613-0073},
	Month = jul,
	Pages = {104-118},
	Series = {CEUR Workshop Proceedings},
	Title = {A Termination Checker for {Isabelle} {Hoare} Logic},
	Url = {http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-259/paper10.pdf},
	Volume = {259},
	Year = {2007},
	Bdsk-Url-1 = {http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-259/paper10.pdf}}

@conference{akbarpour-towards,
	Author = {Behzad Akbarpour and Lawrence C. Paulson},
	Booktitle = {PDPAR: Pragmatics of Decision Procedures in Automated Reasoning},
	Date-Added = {2008-01-03 10:57:18 +0000},
	Date-Modified = {2008-01-03 10:57:18 +0000},
	Editor = {Byron Cook and Roberto Sebastiani},
	Pages = {27-37},
	Title = {Towards Automatic Proofs of Inequalities Involving Elementary Functions},
	Year = {2006}}

@conference{akbarpour-extending,
	Abstract = {Experiments show that many inequalities involving exponentials and logarithms can be proved automatically by combining a resolution theorem prover with a decision procedure for the theory of real closed fields (RCF). The method should be applicable to any functions for which polynomial upper and lower bounds are known. Most bounds only hold for specific argument ranges, but resolution can automatically perform the necessary case analyses. The system consists of a superposition prover (Metis) combined with John Harrison{\^a}€{\texttrademark}s RCF solver and a small amount of code to simplify literals with respect to the RCF theory. },
	Author = {Akbarpour, Behzad and Paulson, Lawrence},
	Booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning},
	Date-Added = {2008-01-03 10:57:10 +0000},
	Date-Modified = {2008-01-03 10:57:10 +0000},
	Doi = {10.1007/978-3-540-75560-9_6},
	Pages = {47-61},
	Title = {Extending a Resolution Prover for Inequalities on Elementary Functions},
	Url = {http://dx.doi.org/10.1007/978-3-540-75560-9_6},
	Year = {2007},
	Bdsk-Url-1 = {http://dx.doi.org/10.1007/978-3-540-75560-9_6}}

@article{meng-translating,
	Author = {Jia Meng and Lawrence C. Paulson},
	Date-Added = {2008-01-03 10:48:28 +0000},
	Date-Modified = {2008-01-03 10:48:28 +0000},
	Doi = {10.1007/s10817-007-9085-y},
	Journal = jar,
	Month = jan,
	Number = {1},
	Pages = {35-60},
	Title = {Translating Higher-Order Problems to First-Order Clauses},
	Volume = {40},
	Year = {2008},
	Bdsk-Url-1 = {http://dx.doi.org/10.1007/s10817-007-9085-y}}

@proceedings{escor06,
	Booktitle = {FLoC'06 Workshop on Empirically Successful Computerized Reasoning},
	Date-Added = {2008-01-03 10:44:25 +0000},
	Date-Modified = {2008-01-03 10:44:25 +0000},
	Editor = {Sutcliffe, Geoff and Schmidt, Renate and Schulz, Schulz},
	Series = {CEUR Workshop Proceedings},
	Title = {FLoC'06 Workshop on Empirically Successful Computerized Reasoning},
	Url = {http://CEUR-WS.org/Vol-192/},
	Volume = {192},
	Year = {2006},
	Bdsk-Url-1 = {http://CEUR-WS.org/Vol-192/}}

@inproceedings{meng-translating-escor,
	Author = {Jia Meng and Lawrence C. Paulson},
	Crossref = {escor06},
	Date-Added = {2008-01-03 10:43:45 +0000},
	Date-Modified = {2008-01-03 10:43:45 +0000},
	Pages = {70-80},
	Title = {Translating Higher-Order Problems to First-Order Clauses}}

@inproceedings{meng-relevance-escor,
	Author = {Jia Meng and Lawrence C. Paulson},
	Crossref = {escor06},
	Date-Added = {2008-01-03 10:43:39 +0000},
	Date-Modified = {2008-01-03 10:43:39 +0000},
	Local-Url = {file://localhost/Users/lcp/Internet/LCP's%20Web%20Site/papers/Automation/filtering.pdf},
	Pages = {53-69},
	Title = {Lightweight Relevance Filtering for Machine-Generated Resolution Problems}}

@article{bella-accountability,
	Author = {Giampaolo Bella and Lawrence C. Paulson},
	Date-Added = {2008-01-03 10:42:44 +0000},
	Date-Modified = {2008-01-03 10:42:44 +0000},
	Doi = {10.1145/1151414.1151416},
	Issn = {1094-9224},
	Journal = {ACM Trans. Inf. Syst. Secur.},
	Number = {2},
	Pages = {138-161},
	Publisher = {ACM Press},
	Title = {Accountability protocols: Formalized and verified},
	Url = {http://doi.acm.org/10.1145/1151414.1151416},
	Volume = {9},
	Year = {2006},
	Bdsk-Url-1 = {http://doi.acm.org/10.1145/1151414.1151416},
	Bdsk-Url-2 = {http://dx.doi.org/10.1145/1151414.1151416}}

@article{set-purchase,
	Author = {Giampaolo Bella and Fabio Massacci and Lawrence C. Paulson},
	Date-Added = {2008-01-03 10:42:18 +0000},
	Date-Modified = {2008-01-03 10:42:18 +0000},
	Doi = {10.1007/s10817-005-9018-6},
	Journal = JAR,
	Pages = {5-37},
	Title = {Verifying the {SET} Purchase Protocols},
	Volume = {36},
	Year = {2006},
	Bdsk-Url-1 = {http://dx.doi.org/10.1007/s10817-005-9018-6}}

@article{paulson-equiv,
	Author = {Lawrence C. Paulson},
	Date-Added = {2008-01-03 10:41:06 +0000},
	Date-Modified = {2008-01-03 10:41:06 +0000},
	Doi = {10.1145/1166109.1166111},
	Issn = {1529-3785},
	Journal = TOCL,
	Number = {4},
	Pages = {658-675},
	Publisher = {ACM Press},
	Title = {Defining Functions on Equivalence Classes},
	Url = {http://doi.acm.org/10.1145/1166109.1166111},
	Volume = {7},
	Year = {2006},
	Bdsk-Url-1 = {http://doi.acm.org/10.1145/1166109.1166111},
	Bdsk-Url-2 = {http://dx.doi.org/10.1145/1166109.1166111}}

@inproceedings{fleuriot-adg,
	Author = {Fleuriot, Jacques and Paulson, Lawrence C.},
	Booktitle = {Workshop on Automated Deduction in Geometry, Second International Workshop, ADG'98},
	Date-Added = {2006-08-30 11:20:31 +0100},
	Date-Modified = {2006-08-30 11:25:39 +0100},
	Editor = {Xiao-Shan Gao and Dongming Wang and Lu Yang},
	Pages = {47-66},
	Publisher = {Springer},
	Series = {LNCS 1669},
	Title = {Proving {Newton's} \emph{Propositio Kepleriana} Using Geometry and Nonstandard Analysis in {Isabelle}},
	Year = {1999}}

@article{meng-automation,
	Author = {Jia Meng and Claire Quigley and Lawrence C. Paulson},
	Booktitle = {Automation for Interactive Proof: First Prototype},
	Date-Added = {2006-02-10 16:32:33 +0000},
	Date-Modified = {2006-09-18 10:11:54 +0100},
	Doi = {j.ic.2005.05.010},
	Journal = {Information and Computation},
	Number = {10},
	Pages = {1575-1596},
	Title = {Automation for Interactive Proof: First Prototype},
	Url = {http://www.sciencedirect.com/science/article/B6WGK-4K9C6J3-1/2/e4e5661335eef1bb58ed32a67a7f2427},
	Volume = {204},
	Year = {2006},
	Bdsk-Url-1 = {http://www.sciencedirect.com/science/article/B6WGK-4K9C6J3-1/2/e4e5661335eef1bb58ed32a67a7f2427},
	Bdsk-Url-2 = {http://dx.doi.org/2005.05.010}}

@article{ehmety-lessons,
	Author = {Sidi O. Ehmety and L. C. Paulson},
	Date-Added = {2005-07-08 15:03:26 +0100},
	Date-Modified = {2005-10-20 14:46:28 +0100},
	Doi = {10.1007/s00165-004-0053-6},
	Journal = {Formal Aspects of Computing},
	Month = {may},
	Number = {1},
	Pages = {58-68},
	Title = {Mechanizing Compositional Reasoning for Concurrent Systems: Some Lessons},
	Volume = {17},
	Year = {2005},
	Bdsk-Url-1 = {http://dx.doi.org/10.1007/s00165-004-0053-6}}

@inproceedings{nipkow-defining,
	Author = {Tobias Nipkow and Lawrence C. Paulson},
	Booktitle = {Theorem Proving in Higher Order Logics: TPHOLs 2005},
	Date-Modified = {2005-10-20 14:56:27 +0100},
	Doi = {10.1007/11541868_25},
	Editor = {Joe Hurd and Tom Melham},
	Pages = {385-396},
	Publisher = Springer,
	Series = {LNCS 3603},
	Title = {Proof Pearl: Defining Functions Over Finite Sets},
	Year = 2005,
	Bdsk-Url-1 = {http://dx.doi.org/10.1007/11541868_25}}

@phdthesis{paulson-thesis,
	Author = {Lawrence C. Paulson},
	School = {Stanford University},
	Title = {A Compiler Generator for Semantic Grammars},
	Year = {1981}}

@inproceedings{paulson-popl,
	Author = {Lawrence Paulson},
	Booktitle = {Ninth Annual ACM Symposium on Principles of Programming Languages},
	Date-Modified = {2005-04-20 13:58:40 +0100},
	Pages = {224-233},
	Publisher = {ACM Press},
	Title = {A Semantics-Directed Compiler Generator},
	Year = {1982}}

@article{paulson83,
	Author = {Lawrence C. Paulson},
	Date-Modified = {2005-04-20 13:23:42 +0100},
	Journal = {Science of Computer Programming},
	Pages = {119-149},
	Title = {A Higher-Order Implementation of Rewriting},
	Volume = {3},
	Year = {1983}}

@inproceedings{paulson84,
	Author = {Lawrence C. Paulson},
	Booktitle = {Semantics of Data Types},
	Editor = {G. Kahn and D. B. MacQueen and G. Plotkin},
	Note = {LNCS 173},
	Pages = {197-214},
	Publisher = {Springer},
	Title = {Deriving Structural Induction in {LCF}},
	Year = {1984}}

@article{paulson85,
	Author = {Lawrence C. Paulson},
	Date-Modified = {2005-04-20 13:24:23 +0100},
	Journal = {Science of Computer Programming},
	Pages = {143-170},
	Title = {Verifying the Unification Algorithm in {LCF}},
	Volume = {5},
	Year = {1985}}

@article{paulson-lessons,
	Author = {Lawrence C. Paulson},
	Date-Added = {2005-04-20 14:00:35 +0100},
	Date-Modified = {2005-04-20 14:01:59 +0100},
	Journal = {Computer Journal},
	Pages = {474-479},
	Title = {Lessons learned from {LCF}: a Survey of Natural Deduction Proofs},
	Volume = {28},
	Year = {1985}}

@article{paulson-cons,
	Author = {Lawrence C. Paulson},
	Date-Modified = {2005-04-21 17:28:51 +0100},
	Journal = {Journal of Symbolic Computation},
	Pages = {325-355},
	Title = {Constructing Recursion Operators in Intuitionistic Type Theory},
	Volume = {2},
	Year = {1986}}

@article{paulson-norm,
	Author = {Lawrence C. Paulson},
	Date-Modified = {2005-04-21 17:29:20 +0100},
	Doi = {10.1007/BF00246023},
	Journal = {Journal of Automated Reasoning},
	Pages = {63-74},
	Title = {Proving Termination of Normalization Functions for Conditional Expressions},
	Volume = {2},
	Year = {1986},
	Bdsk-Url-1 = {http://dx.doi.org/10.1007/BF00246023}}

@article{paulson86,
	Author = {Lawrence C. Paulson},
	Date-Modified = {2005-04-21 17:29:40 +0100},
	Journal = {Journal of Logic Programming},
	Pages = {237-258},
	Title = {Natural Deduction as Higher-order Resolution},
	Volume = {3},
	Year = {1986}}

@book{paulson87,
	Author = {Lawrence C. Paulson},
	Publisher = {Cambridge University Press},
	Title = {Logic and Computation: Interactive proof with Cambridge LCF},
	Year = {1987}}

@inproceedings{paulson88,
	Author = {Lawrence C. Paulson},
	Booktitle = {Ninth International Conference on Automated Deduction},
	Crossref = {cade9},
	Date-Modified = {2005-04-20 12:20:38 +0100},
	Editor = {E. Lusk and R. Overbeek},
	Pages = {772-773},
	Publisher = {Springer},
	Series = {LNCS 310},
	Title = {Isabelle: The Next Seven Hundred Theorem Provers (system abstract)},
	Year = {1988}}

@techreport{paulson-manual,
	Author = {Lawrence C. Paulson},
	Institution = {Computer Laboratory, University of Cambridge},
	Number = {133},
	Title = {A preliminary user's manual for {Isabelle}},
	Year = {1988}}

@article{paulson89,
	Author = {Lawrence C. Paulson},
	Date-Modified = {2005-04-22 15:30:48 +0100},
	Journal = {Journal of Automated Reasoning},
	Number = {3},
	Pages = {363-397},
	Title = {The Foundation of a Generic Theorem Prover},
	Volume = {5},
	Year = {1989}}

@techreport{paulson90,
	Author = {Lawrence C. Paulson and Tobias Nipkow},
	Institution = {Computer Laboratory, University of Cambridge},
	Month = Jan,
	Number = {189},
	Title = {{Isabelle} Tutorial and User's Manual},
	Year = {1990}}

@inproceedings{paulson-COLOG,
	Author = {Lawrence C. Paulson},
	Booktitle = {COLOG-88: International Conference on Computer Logic},
	Date-Modified = {2005-04-20 12:10:19 +0100},
	Editor = {P. Martin-L{\"o}f and G. Mints},
	Pages = {246-274},
	Publisher = {Springer},
	Series = {LNCS 417},
	Title = {A Formulation of the Simple Theory of Types (for {Isabelle})},
	Year = {1990}}

@incollection{paulson700,
	Author = {Lawrence C. Paulson},
	Booktitle = {Logic and Computer Science},
	Date-Modified = {2005-04-20 12:07:55 +0100},
	Editor = {P. Odifreddi},
	Pages = {361-386},
	Publisher = {Academic Press},
	Title = {{Isabelle}: The Next 700 Theorem Provers},
	Year = {1990}}

@book{paulson91,
	Author = {Lawrence C. Paulson},
	Publisher = {Cambridge University Press},
	Title = {{ML} for the Working Programmer},
	Year = {1991}}

@inproceedings{paulson-smith,
	Author = {Lawrence C. Paulson and Andrew W. Smith},
	Booktitle = {Extensions of Logic Programming},
	Date-Modified = {2005-04-25 17:12:46 +0100},
	Editor = {Peter Schroeder-Heister},
	Pages = {283-310},
	Publisher = {Springer},
	Series = {LNAI 475},
	Title = {Logic Programming, Functional Programming, and Inductive Definitions},
	Year = {1991}}

@inproceedings{nipkow-paulson92,
	Author = {Tobias Nipkow and Lawrence C. Paulson},
	Booktitle = {Automated Deduction --- {CADE}-11},
	Date-Modified = {2005-04-20 12:06:09 +0100},
	Editor = {Deepak Kapur},
	Pages = {673-676},
	Publisher = {Springer},
	Series = {LNAI 607},
	Title = {{Isabelle}-91 (system abstract)},
	Year = {1992}}

@incollection{paulson-handbook,
	Author = {Lawrence C. Paulson},
	Booktitle = {Handbook of Logic in Computer Science},
	Date-Modified = {2005-04-20 13:17:43 +0100},
	Editor = {S. Abramsky and D. M. Gabbay and T. S. E. Maibaum},
	Pages = {415-475},
	Publisher = {Oxford University Press},
	Title = {Designing a Theorem Prover},
	Volume = {2},
	Year = {1992}}

@techreport{paulson-set-I-tr,
	Author = {Lawrence C. Paulson},
	Institution = {Computer Laboratory, University of Cambridge},
	Number = {271},
	Title = {Set Theory as a Computational Logic: {I}. {From} Foundations to Functions},
	Year = {1992}}

@article{paulson-set-I,
	Author = {Lawrence C. Paulson},
	Date-Modified = {2005-04-26 09:57:55 +0100},
	Journal = {Journal of Automated Reasoning},
	Number = {3},
	Pages = {353-389},
	Title = {Set Theory for Verification: {I}. {From} Foundations to Functions},
	Volume = {11},
	Year = {1993}}

@techreport{isabelle-intro,
	Author = {Lawrence C. Paulson},
	Date-Modified = {2005-04-26 10:12:43 +0100},
	Institution = {Computer Laboratory, University of Cambridge},
	Number = {280},
	Title = {Introduction to {Isabelle}},
	Year = {1993}}

@techreport{isabelle-ref,
	Author = {Lawrence C. Paulson},
	Date-Modified = {2005-04-26 10:12:56 +0100},
	Institution = {Computer Laboratory, University of Cambridge},
	Number = {283},
	Title = {The {Isabelle} Reference Manual},
	Year = {1993}}

@techreport{paulson-set-II-tr,
	Author = {Lawrence C. Paulson},
	Date-Modified = {2005-04-26 10:13:06 +0100},
	Institution = {Computer Laboratory, University of Cambridge},
	Number = {312},
	Title = {Set Theory for Verification: {II}. {Induction} and Recursion},
	Year = {1993}}

@techreport{isabelle-logics,
	Author = {Lawrence C. Paulson},
	Institution = {Computer Laboratory, University of Cambridge},
	Number = {286},
	Title = {{Isabelle}'s Object-Logics},
	Year = {1993}}

@techreport{paulson-fixedpt,
	Author = {Lawrence C. Paulson},
	Institution = {Computer Laboratory, University of Cambridge},
	Month = Dec,
	Number = {320},
	Title = {A Fixedpoint Approach to Implementing (Co)Inductive Definitions},
	Year = {1993}}

@inproceedings{paulson-CADE,
	Author = {Lawrence C. Paulson},
	Booktitle = {Automated Deduction --- {CADE}-12},
	Date-Modified = {2005-04-20 12:17:47 +0100},
	Editor = {Alan Bundy},
	Pages = {148-161},
	Publisher = {Springer},
	Series = {LNAI 814},
	Title = {A Fixedpoint Approach to Implementing (Co)Inductive Definitions},
	Year = {1994}}

@book{paulson-isa-book,
	Author = {Lawrence C. Paulson},
	Note = {LNCS 828},
	Publisher = {Springer},
	Title = {Isabelle: A Generic Theorem Prover},
	Year = {1994}}

@article{paulson-set-II,
	Author = {Lawrence C. Paulson},
	Journal = {Journal of Automated Reasoning},
	Number = {2},
	Pages = {167-215},
	Title = {Set Theory for Verification: {II}. {Induction} and Recursion},
	Volume = {15},
	Year = {1995}}

@inproceedings{paulson-final,
	Author = {Lawrence C. Paulson},
	Booktitle = {Types for Proofs and Programs: International Workshop {TYPES '94}},
	Date-Modified = {2005-04-20 12:11:46 +0100},
	Editor = {Peter Dybjer and Bengt Nordstr{\"om} and Jan Smith},
	Pages = {120-139},
	Publisher = {Springer},
	Series = {LNCS 996},
	Title = {A Concrete Final Coalgebra Theorem for {ZF} Set Theory},
	Year = {1995}}

@proceedings{isabelle-ws,
	Booktitle = {Proceedings of the First Isabelle Users Workshop},
	Date-Modified = {2005-04-20 13:26:50 +0100},
	Editor = {Lawrence C. Paulson},
	Month = sep,
	Organization = {Computer Laboratory, University of Cambridge},
	Series = {Technical Report 379},
	Title = {First Isabelle Users Workshop},
	Year = {1995}}

@book{paulson-ml2,
	Author = {Lawrence C. Paulson},
	Edition = {2nd},
	Publisher = {Cambridge University Press},
	Title = {{ML} for the Working Programmer},
	Year = {1996}}

@techreport{paulson-mutil,
	Author = {Lawrence C. Paulson},
	Institution = {Computer Laboratory, University of Cambridge},
	Month = May,
	Number = {394},
	Title = {A Simple Formalization and Proof for the Mutilated Chess Board},
	Year = {1996}}

@article{paulson-gr,
	Author = {Lawrence C. Paulson and Krzysztof Gr\c{a}bczewski},
	Journal = {Journal of Automated Reasoning},
	Month = dec,
	Number = {3},
	Pages = {291-323},
	Title = {Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of Choice},
	Volume = {17},
	Year = {1996}}

@techreport{paulson-ns,
	Author = {Lawrence C. Paulson},
	Institution = {Computer Laboratory, University of Cambridge},
	Month = Jan,
	Number = {413},
	Title = {Mechanized Proofs of Security Protocols: {Needham-Schroeder} with Public Keys},
	Year = {1997}}

@article{paulson-coind,
	Author = {Lawrence C. Paulson},
	Date-Modified = {2005-04-27 12:14:37 +0100},
	Journal = {Journal of Logic and Computation},
	Month = apr,
	Number = {2},
	Pages = {175-204},
	Title = {Mechanizing Coinduction and Corecursion in Higher-Order Logic},
	Volume = {7},
	Year = {1997}}

@inproceedings{paulson-security,
	Author = {Lawrence C. Paulson},
	Booktitle = {10th Computer Security Foundations Workshop},
	Date-Modified = {2005-04-27 12:22:07 +0100},
	Pages = {70-83},
	Publisher = {IEEE Computer Society Press},
	Title = {Proving Properties of Security Protocols by Induction},
	Year = {1997}}

@incollection{paulson-markt,
	Author = {Lawrence C. Paulson},
	Booktitle = {Mathematical Methods in Program Development: Summer School Marktoberdorf 1996},
	Date-Modified = {2009-03-06 15:52:07 +0000},
	Editor = {Manfred Broy and Birgit Schieder},
	Pages = {461-498},
	Publisher = {Springer},
	Series = {NATO ASI Series F},
	Title = {Tool Support for Logics of Programs},
	Year = {1997}}

@inproceedings{paulson-recur,
	Author = {Lawrence C. Paulson},
	Booktitle = {10th Computer Security Foundations Workshop},
	Crossref = {csfw10},
	Date-Modified = {2005-04-20 13:22:19 +0100},
	Pages = {84-95},
	Publisher = {IEEE Computer Society Press},
	Title = {Mechanized Proofs for a Recursive Authentication Protocol},
	Year = {1997}}

@incollection{paulson-generic,
	Author = {Lawrence C. Paulson},
	Booktitle = {Automated Reasoning and its Applications: Essays in Honor of {Larry Wos}},
	Chapter = {3},
	Crossref = {wos-fest},
	Date-Modified = {2005-04-20 13:20:25 +0100},
	Editor = {Robert Veroff},
	Publisher = {MIT Press},
	Title = {Generic Automatic Proof Tools},
	Year = {1997}}

@inproceedings{bella-kerberos,
	Author = {Giampaolo Bella and Lawrence C. Paulson},
	Booktitle = {Workshop on Design and Formal Verification of Security Protocols},
	Date-Modified = {2005-04-20 12:03:35 +0100},
	Editor = {Hilarie Orman and Catherine Meadows},
	Month = {Sep},
	Organization = {DIMACS},
	Title = {Using {Isabelle} to Prove Properties of the {Kerberos} Authentication System},
	Year = {1997}}

@inproceedings{paulson-blast-cade,
	Author = {Lawrence C. Paulson},
	Booktitle = {CADE-15 Workshop on Integration of Deduction Systems},
	Editor = {Nikolaj S. Bj{\o}rner et al},
	Pages = {51-60},
	Title = {A Generic Tableau Prover and its Integration with {Isabelle} (Extended Abstract)},
	Year = {1998}}

@inproceedings{bella-kerberos4,
	Author = {Giampaolo Bella and Lawrence C. Paulson},
	Booktitle = {Computer Security --- {ESORICS} 98},
	Date-Modified = {2005-04-20 11:58:27 +0100},
	Editor = {J.-J. Quisquater and Y. Deswarte and C. Meadows and D. Gollmann},
	Pages = {361-375},
	Publisher = {Springer},
	Series = {LNCS 1485},
	Title = {{Kerberos} Version {IV}: Inductive Analysis of the Secrecy Goals},
	Year = {1998}}

@inproceedings{bella-ban-kerberos,
	Author = {Giampaolo Bella and Lawrence C. Paulson},
	Booktitle = {Computer Aided Verification: 10th International Conference, {CAV} '98},
	Date-Modified = {2005-04-20 11:44:54 +0100},
	Editor = {Alan J. Hu and Moshe Y. Vardi},
	Pages = {416-427},
	Publisher = {Springer},
	Title = {Mechanising {BAN} {Kerberos} by the Inductive Method},
	Year = {1998}}

@inproceedings{ballarin-coding,
	Author = {Clemens Ballarin and Lawrence C. Paulson},
	Booktitle = {Artificial Intelligence and Symbolic Computation: International Conference AISC'98},
	Date-Modified = {2005-04-20 11:42:36 +0100},
	Editor = {Jacques Calmet and Jan Plaza},
	Pages = {55-66},
	Publisher = {Springer},
	Series = {LNAI 1476},
	Title = {Reasoning about Coding Theory: The Benefits we get from Computer Algebra},
	Year = {1998}}

@article{paulson-jcs,
	Author = {Lawrence C. Paulson},
	Date-Modified = {2005-05-04 15:09:37 +0100},
	Journal = {Journal of Computer Security},
	Number = {1-2},
	Pages = {85-128},
	Title = {The Inductive Approach to Verifying Cryptographic Protocols},
	Volume = {6},
	Year = {1998}}

@inproceedings{fleuriot-cade,
	Author = {Fleuriot, Jacques and Paulson, Lawrence C.},
	Booktitle = {Automated Deduction --- {CADE}-15 International Conference},
	Date-Modified = {2005-04-20 13:45:41 +0100},
	Editor = {Claude Kirchner and {H\'el\`ene} Kirchner},
	Pages = {3-16},
	Publisher = {Springer},
	Series = {LNAI 1421},
	Title = {A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to {Newton's} \emph{Principia}},
	Year = {1998}}

@article{paulson-blast,
	Author = {Lawrence C. Paulson},
	Date-Modified = {2005-05-04 15:28:31 +0100},
	Journal = {Journal of Universal Computer Science},
	Number = {3},
	Title = {A Generic Tableau Prover and its Integration with {Isabelle}},
	Url = {http://www.jucs.org/jucs_5_3/a_generic_tableau_prover},
	Volume = {5},
	Year = {1999},
	Bdsk-Url-1 = {http://www.jucs.org/jucs_5_3/a_generic_tableau_prover}}

@inproceedings{paulson-lics,
	Author = {Lawrence C. Paulson},
	Booktitle = {14th Annual Symposium on Logic in Computer Science},
	Crossref = {lics14},
	Date-Modified = {2005-04-20 12:09:05 +0100},
	Organization = {IEEE},
	Pages = {370-381},
	Title = {Proving Security Protocols Correct},
	Year = {1999}}

@inproceedings{kammueller-locales,
	Author = {Florian Kamm{\"u}ller and Markus Wenzel and Lawrence C. Paulson},
	Booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
	Date-Modified = {2005-04-20 11:49:28 +0100},
	Editor = {Yves Bertot and Gilles Dowek and Andr{\'e} Hirschowitz and Christine Paulin and Laurent Th{\'e}ry},
	Pages = {149-165},
	Publisher = {Springer},
	Title = {Locales: A Sectioning Concept for {Isabelle}},
	Year = {1999}}

@article{ballarin-pragmatic,
	Author = {Clemens Ballarin and Lawrence C. Paulson},
	Journal = {Fundamenta Informaticae},
	Pages = {1-20},
	Title = {A Pragmatic Approach to Extending Provers by Computer Algebra --- with Applications to Coding Theory},
	Volume = {39},
	Year = {1999}}

@article{kammueller-sylow,
	Author = {Florian Kamm{\"u}ller and L. C. Paulson},
	Date-Modified = {2005-05-04 16:49:50 +0100},
	Doi = {10.1023/A:1006269330992},
	Journal = {Journal of Automated Reasoning},
	Number = {3-4},
	Pages = {235-264},
	Title = {A Formal Proof of {Sylow}'s theorem: An Experiment in Abstract Algebra with {Isabelle HOL}},
	Volume = {23},
	Year = {1999},
	Bdsk-Url-1 = {http://dx.doi.org/10.1023/A:1006269330992}}

@article{paulson-mscs,
	Author = {Lawrence C. Paulson},
	Date-Modified = {2005-05-17 14:25:55 +0100},
	Journal = {Mathematical Structures in Computer Science},
	Month = oct,
	Number = {5},
	Pages = {545-567},
	Title = {Final Coalgebras as Greatest Fixed Points in {ZF} Set Theory},
	Volume = {9},
	Year = {1999}}

@article{lamport-paulson-types,
	Author = {Leslie Lamport and Lawrence C. Paulson},
	Date-Modified = {2005-04-20 13:38:25 +0100},
	Journal = {ACM Transactions on Programming Languages and Systems},
	Month = may,
	Number = {3},
	Pages = {502-526},
	Title = {Should Your Specification Language Be Typed?},
	Volume = {21},
	Year = {1999}}

@article{paulson-tls,
	Author = {Lawrence C. Paulson},
	Journal = {ACM Transactions on Information and System Security},
	Month = aug,
	Number = {3},
	Pages = {332-351},
	Title = {Inductive Analysis of the {Internet} Protocol {TLS}},
	Volume = {2},
	Year = {1999}}

@article{fleuriot-jcm,
	Author = {Jacques D. Fleuriot and Lawrence C. Paulson},
	Journal = {LMS Journal of Computation and Mathematics},
	Note = {\url{http://old.lms.ac.uk/jcm//3/lms1999-027/?q=jcm/3/lms1999-027/}},
	Pages = {140-190},
	Title = {Mechanizing Nonstandard Real Analysis},
	Volume = {3},
	Year = {2000}}

@article{paulson-unity,
	Author = {Lawrence C. Paulson},
	Date-Modified = {2005-04-20 13:39:03 +0100},
	Journal = {ACM Transactions on Computational Logic},
	Number = {1},
	Pages = {3-32},
	Title = {Mechanizing {UNITY} in {Isabelle}},
	Volume = {1},
	Year = {2000}}

@incollection{paulson-fixedpt-milner,
	Author = {Lawrence C. Paulson},
	Booktitle = {Proof, Language, and Interaction: Essays in Honor of {Robin Milner}},
	Crossref = {milner-fest},
	Date-Modified = {2005-04-20 14:16:25 +0100},
	Editor = {Gordon Plotkin and Colin Stirling and Mads Tofte},
	Pages = {187-211},
	Publisher = {MIT Press},
	Title = {A Fixedpoint Approach to (Co)inductive and (Co)datatype Definitions},
	Year = {2000}}

@inproceedings{set-esorics,
	Author = {Giampaolo Bella and Fabio Massacci and Lawrence C. Paulson and Piero Tramontano},
	Booktitle = {Computer Security --- {ESORICS} 2000},
	Date-Modified = {2005-04-20 11:52:32 +0100},
	Editor = {F. Cuppens and Y. Deswarte and D. Gollman and M. Waidner},
	Pages = {159-174},
	Publisher = {Springer},
	Series = {LNCS 1895},
	Title = {Formal Verification of Cardholder Registration in {SET}},
	Year = {2000}}

@article{paulson-unity2,
	Author = {Lawrence C. Paulson},
	Date-Modified = {2005-04-20 13:47:19 +0100},
	Journal = {ACM Transactions on Programming Languages and Systems},
	Number = {5},
	Pages = {626-656},
	Title = {Mechanizing a Theory of Program Composition for {UNITY}},
	Volume = {25},
	Year = {2001}}

@inproceedings{bella-nonrepud,
	Author = {Giampaolo Bella and Lawrence C. Paulson},
	Booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} 2001},
	Date-Modified = {2005-04-20 11:54:34 +0100},
	Editor = {Richard J. Boulton and Paul B. Jackson},
	Pages = {91-104},
	Publisher = {Springer},
	Series = {LNCS 2152},
	Title = {Mechanical Proofs about a Non-Repudiation Protocol},
	Year = {2001}}

@article{paulson-mutil01,
	Author = {Lawrence C. Paulson},
	Date-Modified = {2008-11-06 10:38:26 +0000},
	Doi = {10.1093/jigpal/9.3.475},
	Journal = {Logic Journal of the IGPL},
	Number = {3},
	Pages = {499-509},
	Title = {A Simple Formalization and Proof for the Mutilated Chess Board},
	Url = {http://jigpal.oxfordjournals.org/content/vol9/issue3/},
	Volume = {9},
	Year = {2001},
	Bdsk-Url-1 = {http://www3.oup.co.uk/igpl/Volume_09/Issue_03/}}

@inproceedings{paulson-ijcar,
	Author = {Lawrence C. Paulson},
	Booktitle = {Automated Reasoning --- First International Joint Conference, IJCAR 2001},
	Date-Modified = {2005-04-20 13:16:31 +0100},
	Editor = {Rajeev Gor{\'e} and Alexander Leitsch and Tobias Nipkow},
	Pages = {5-12},
	Publisher = {Springer},
	Series = {LNAI 2083},
	Title = {{SET} Cardholder Registration: the Secrecy Proofs},
	Year = {2001}}

@article{paulson-yahalom,
	Author = {Lawrence C. Paulson},
	Date-Modified = {2005-04-20 13:46:42 +0100},
	Journal = {Journal of Computer Security},
	Number = {3},
	Pages = {197-216},
	Title = {Relations Between Secrets: Two Formal Analyses of the {Yahalom} Protocol},
	Volume = {9},
	Year = {2001}}

@book{isa-tutorial,
	Author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
	Note = {LNCS Tutorial 2283},
	Publisher = {Springer},
	Title = {Isabelle/HOL: A Proof Assistant for Higher-Order Logic},
	Year = {2002}}

@inproceedings{ehmety-composition,
	Author = {Sidi O. Ehmety and Lawrence C. Paulson},
	Booktitle = {Workshop on Formal Methods for Parallel Programming: Theory and Applications; text on CD-ROM},
	Date-Modified = {2005-04-20 14:21:12 +0100},
	Editor = {Michel Charpentier and Beverly Sanders},
	Organization = {IEEE},
	Title = {Program Composition in {Isabelle/UNITY}},
	Year = {2002}}

@inproceedings{paulson-reflection,
	Author = {Lawrence C. Paulson},
	Booktitle = {Automated Deduction --- {CADE}-18 International Conference},
	Date-Modified = {2005-04-20 13:19:39 +0100},
	Editor = {Andrei Voronkov},
	Pages = {377-391},
	Publisher = {Springer},
	Series = {LNAI 2392},
	Title = {The Reflection Theorem: A Study in Meta-Theoretic Reasoning},
	Year = {2002}}

@inproceedings{set-purchase-ccs,
	Author = {Giampaolo Bella and Fabio Massacci and Lawrence C. Paulson},
	Booktitle = {9th {ACM} Conference on Computer and Communications Security},
	Editor = {Vijay Atluri},
	Pages = {12-20},
	Publisher = {ACM Press},
	Title = {The Verification of an Industrial Payment Protocol: The {SET} Purchase Phase},
	Year = {2002}}

@article{paulson-consistency,
	Author = {Lawrence C. Paulson},
	Journal = {LMS Journal of Computation and Mathematics},
	Note = {\url{http://old.lms.ac.uk/jcm/6/lms2003-001/?q=jcm/6/lms2003-001/}},
	Pages = {198-248},
	Title = {The Relative Consistency of the Axiom of Choice --- Mechanized Using {Isabelle/ZF}},
	Volume = {6},
	Year = {2003}}

@article{set-registration,
	Author = {Giampaolo Bella and Fabio Massacci and Lawrence C. Paulson},
	Date-Modified = {2005-05-25 16:40:42 +0100},
	Doi = {10.1109/JSAC.2002.806133},
	Journal = {IEEE Journal on Selected Areas in Communications},
	Number = {1},
	Pages = {77-87},
	Title = {Verifying the {SET} Registration Protocols},
	Volume = {21},
	Year = {2003},
	Bdsk-Url-1 = {http://dx.doi.org/10.1109/JSAC.2002.806133}}

@inproceedings{bella-second,
	Author = {Giampaolo Bella and Cristiano Longo and Lawrence C. Paulson},
	Booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} 2003},
	Date-Modified = {2005-04-20 11:51:32 +0100},
	Editor = {David Basin and Burkhart Wolff},
	Pages = {352-366},
	Publisher = {Springer},
	Series = {LNCS 2758},
	Title = {Verifying Second-Level Security Protocols},
	Year = {2003}}

@inproceedings{meng-experiments,
	Author = {Jia Meng and Lawrence C. Paulson},
	Booktitle = {Automated Reasoning --- Second International Joint Conference, IJCAR 2004},
	Date-Modified = {2005-04-20 14:31:43 +0100},
	Doi = {10.1007/b98691},
	Editor = {David Basin and Micha{\"e}l Rusinowitch},
	Pages = {372-384},
	Publisher = {Springer},
	Series = {LNAI 3097},
	Title = {Experiments On Supporting Interactive Proof Using Resolution},
	Year = {2004},
	Bdsk-Url-1 = {http://dx.doi.org/10.1007/b98691}}

@article{paulson-numerical,
	Author = {Lawrence C. Paulson},
	Date-Modified = {2005-04-20 14:37:30 +0100},
	Journal = {Journal of Automated Reasoning},
	Number = {1},
	Pages = {29-49},
	Title = {Organizing Numerical Theories Using Axiomatic Type Classes},
	Volume = {33},
	Year = {2004}}

@article{bella-overview,
	Author = {Giampaolo Bella and Fabio Massacci and Lawrence C. Paulson},
	Date-Modified = {2005-04-20 13:54:15 +0100},
	Doi = {10.1007/s10207-004-0047-7},
	Journal = {International Journal of Information Security},
	Number = {1-2},
	Pages = {17-28},
	Title = {An Overview of the Verification of {SET}},
	Url = {http://www.springerlink.com/index/10.1007/s10207-004-0047-7},
	Volume = {4},
	Year = {2005},
	Bdsk-Url-1 = {http://www.springerlink.com/index/10.1007/s10207-004-0047-7},
	Bdsk-Url-2 = {http://dx.doi.org/10.1007/s10207-004-0047-7}}