Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Refereed Articles
[go: Go Back, main page]

Refereed Articles

A BibTeX file of these articles is available.

  1. L. C. Paulson.
    A semantics-directed compiler generator. Principles of Programming Languages (1982), 224–233.
  2. L. C. Paulson.
    A higher-order implementation of rewriting. Science of Computer Programming 3 (1983), 119–149.
  3. L. C. Paulson.
    Deriving structural induction in LCF. In: G. Kahn, D. B. MacQueen, G. Plotkin, editors, Semantics of Data Types (Springer, 1984), 197–214.
  4. L. C. Paulson.
    Verifying the unification algorithm in LCF. Science of Computer Programming 5 (1985), 143–170.
  5. L. C. Paulson.
    Lessons learned from LCF: a Survey of Natural Deduction Proofs. Computer J. 28 (1985), 474–479.
  6. L. C. Paulson.
    Proving termination of normalization functions for conditional expressions. J. Automated Reasoning 2 (1986), 63–74.
  7. L. C. Paulson.
    Constructing recursion operators in Intuitionistic Type Theory. J. Symbolic Computation 2 (1986), 325–355.
  8. L. C. Paulson.
    Natural deduction as higher-order resolution. J. Logic Programming 3 (1986), 237–258.
  9. L. C. Paulson.
    Isabelle: the next seven hundred theorem provers (system abstract). In: E. Lusk and R. Overbeek (editors), 9th International Conf. on Automated Deduction (Springer LNCS 310, 1988), 772–773.
  10. L. C. Paulson.
    The foundation of a generic theorem prover. J. Automated Reasoning 5 (1989), 363–397.
  11. L. C. Paulson.
    A formulation of the simple theory of types (for Isabelle). In: P. Martin-Löf and G. Mints (editors), COLOG-88: International Conf. in Computer Logic.Tallinn, Estonia (1988). Published as Springer LNCS 417, 1990), 246–274.
  12. L. C. Paulson.
    Isabelle: the next 700 theorem provers. In: P. Odifreddi (editor), Logic and Computer Science (Academic Press, 1990), 361–386.
  13. L. C. Paulson.
    Logic programming, functional programming, and inductive definitions. In: P. Schroeder-Heister (editor), Extensions of Logic Programming (Springer, 1991), 283–310. (With A. W. Smith.)
  14. L. C. Paulson.
    Designing a theorem prover. In: S. Abramsky, D. M. Gabbay and T. S. E. Maibaum (editors), Handbook of Logic in Computer Science, Vol II (Oxford, 1992), 415–475.
  15. Tobias Nipkow and L. C. Paulson.
    Isabelle-91 (system abstract). In: D. Kapur (editor), 11th International Conf. on Automated Deduction (Springer LNAI 607, 1992), 673–676.
  16. L. C. Paulson.
    Set theory for verification: I. From foundations to functions. J. Automated Reasoning 11 (1993), 353–389.
  17. L. C. Paulson.
    A fixedpoint approach to implementing (co)inductive definitions. In: A. Bundy (editor), 12th International Conf. on Automated Deduction (Springer LNAI 814, 1994), 148–161.
    Slides available
  18. L. C. Paulson.
    Set theory for verification: II. Induction and recursion. J. Automated Reasoning 15 (1995), 167–215.
  19. L. C. Paulson.
    A concrete final coalgebra theorem for ZF set theory. In: P. Dybjer, B. Nordstrm and J. Smith (editors), Types for Proofs and Programs '94 (Springer LNCS 996, published 1995), 120–139.
  20. L. C. Paulson.
    Mechanizing set theory: cardinal arithmetic and the axiom of choice. J. Automated Reasoning 17 (1996), 291–323. (With Krzysztof Grąbczewski.)
    Slides available
  21. L. C. Paulson.
    Mechanizing coinduction and corecursion in higher-order logic. J. Logic and Computation 7 (March 1997), 175–204.
  22. L. C. Paulson.
    Generic automatic proof tools. In: Robert Veroff (editor), Automated Reasoning and its Applications: Essays in Honor of Larry Wos (MIT Press, 1997), 23–47.
  23. L. C. Paulson.
    Proving properties of security protocols by induction. 10th Computer Security Foundations Workshop (June 1997), 70–83.
    Slides available
  24. L. C. Paulson.
    Mechanized proofs for a recursive authentication protocol. 10th Computer Security Foundations Workshop (June 1997), 84–95.
    Slides:available
  25. Giampaolo Bella and L. C. Paulson.
    Using Isabelle to prove properties of the Kerberos authentication system. DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997.
  26. L. C. Paulson.
    The inductive approach to verifying cryptographic protocols. J. Computer Security 6 (1998), 85–128.
  27. Giampaolo Bella and L. C. Paulson.
    Mechanising BAN Kerberos by the inductive method. In: Alan J. Hu and Moshe Y. Vardi (editors), Computer-Aided Verification: CAV '98 (Springer LNCS 1427, 1998), 416–427.
  28. J. Fleuriot and L. C. Paulson.
    A combination of nonstandard analysis and geometry theorem proving, with application to Newton's Principia (revised version). In: C. Kirchner and H. Kirchner (editors), 15th International Conf. on Automated Deduction: CADE-15 (Springer LNAI 1421, 1998), 3–16.
  29. L. C. Paulson.
    A generic tableau prover and its integration with Isabelle (preliminary version). CADE-15 Workshop on Integration of Deductive Systems (1998), 51–60. Also Report 441, Computer Lab (1998).
    Slides available
  30. C. Ballarin and L. C. Paulson.
    Reasoning about coding theory: the benefits we get from computer algebra. In: Jacques Calmet and Jan Plaza (editors), Artificial Intelligence and Symbolic Computation: AISC '98 (Springer LNAI 1476, 1998), 55–66.
  31. Giampaolo Bella and L. C. Paulson.
    Kerberos version IV: inductive analysis of the secrecy goals. In: Jean-Jacques Quisquater et al. (editors), Computer Security — ESORICS 98 (Springer LNCS 1485, 1998), 361–375.
  32. J. Fleuriot and L. C. Paulson.
    Proving Newton's Propositio Kepleriana Using Geometry and Nonstandard Analysis in Isabelle. In: Xiao-Shan Gao, Dongming Wang and Lu Yang (editors), Automated Deduction in Geometry, Second International Workshop, ADG '98 (Springer LNCS 1669, published 1999), 47–66.
  33. F. Kammüller and L. C. Paulson.
    A formal proof of Sylow's theorem: An experiment in abstract algebra with Isabelle HOL. J. Automated Reasoning 23 (1999), 235–264.
  34. L. C. Paulson.
    Inductive analysis of the Internet protocol TLS. ACM Trans. on Information and System Security 2 3 (1999), 332–351.
    Slides available
  35. L. C. Paulson.
    Final coalgebras as greatest fixed points in ZF set theory. Mathematical Structures in Computer Science 9 (1999), 545–567.
  36. C. Ballarin and L. C. Paulson.
    A pragmatic approach to extending provers by computer algebra — with applications to coding theory. Fundamenta Informaticae 39 (1999), 1–20.
  37. L. Lamport and L. C. Paulson.
    Should your specification language be typed? ACM Trans. on Programming Languages and Systems 21 3 (1999), 502–526.
  38. F. Kammüller, M. Wenzel and L. C. Paulson.
    Locales: A sectioning concept for Isabelle. In: Y. Bertot, G. Dowek, A. Hirshchowitz, Ch. Paulin, L. Théry (editors), Theorem Proving in Higher Order Logics (Springer LNCS 1690, 1999), 149–166.
  39. L. C. Paulson.
    A generic tableau prover and its integration with Isabelle.
    J. Universal Computer Science 5 (3) (1999), 73–87.
  40. L. C. Paulson.
    Mechanizing UNITY in Isabelle. ACM Trans. on Computational Logic 1 1 (2000), 3–32.
  41. L. C. Paulson.
    A fixedpoint approach to (co)inductive and (co)datatype definitions In: G. Plotkin, C. Stirling, and M. Tofte (editors), Proof, Language, and Interaction: Essays in Honour of Robin Milner (MIT Press, 2000), 187–211.
  42. Giampaolo Bella, Fabio Massacci, L. C. Paulson and Piero Tramontano.
    Formal verification of Cardholder Registration in SET. In: F. Cuppens et al. (editors), Computer Security — ESORICS 2000 (Springer LNCS 1895, 2000), 159–174.
  43. Jacques Fleuriot and L. C. Paulson.
    Mechanising nonstandard real analysis.
    LMS J. Computation and Mathematics 3 (2000), 140–190.
  44. L. C. Paulson.
    Relations between secrets: two formal analyses of the Yahalom protocol. J. Computer Security 9 3 (2001), 197–216.
  45. L. C. Paulson.
    A simple formalization and proof for the mutilated chess board.
    Logic J. of the IGPL 9 3 (2001), 499–509.
  46. Giampaolo Bella and L. C. Paulson.
    Mechanical proofs about a non-repudiation protocol. In: Richard J. Boulton and Paul B. Jackson (editors),Theorem Proving in Higher Order Logics (Springer LNCS 2152, 2001), 91–104.
  47. L. C. Paulson.
    Mechanizing a theory of program composition for UNITY. ACM Trans. on Programming Languages and Systems 25 5 (2001), 626–656.
  48. Sidi O. Ehmety and L. C. Paulson.
    Program Composition in Isabelle/UNITY. In: Michel Charpentier and Beverly Sanders (editors),Formal Methods for Parallel Programming: Theory and Application (2002).
  49. L. C. Paulson.
    The reflection theorem: a study in meta-theoretic reasoning.
    In: A. Voronkov (editor), 18th International Conf. on Automated Deduction: CADE-18 (Springer LNAI 2392, 2002), 377–391.
    Slides available
  50. Giampaolo Bella, Fabio Massacci and L. C. Paulson.
    The verification of an industrial payment protocol: the
    SET purchase phase    . In: Vijay Atluri (editor), 9th ACM Conference on Computer and Communications Security (ACM Press, 2002), pages 12–20.
  51. Giampaolo Bella, Fabio Massacci and L. C. Paulson.
    Verifying the SET registration protocols. IEEE Journal on Selected Areas in Communications 21 1 (2003), 77–87.
  52. Giampaolo Bella, Cristiano Longo and L. C. Paulson.
    Verifying second-level security protocols. In: David Basin and Burkhart Wolff (editors),Theorem Proving in Higher Order Logics (Springer LNCS 2758, 2003), pages 352–366.
    Slides available
  53. L. C. Paulson.
    The relative consistency of the axiom of choice mechanized using Isabelle/ZF.
    LMS J. Computation and Mathematics 6 (2003), 198–248.
    Slides and theory document available
  54. Jia Meng and L. C. Paulson.
    Experiments On Supporting Interactive Proof Using Resolution. In: David Basin and Michaël Rusinowitch (editors), IJCAR 2004: Second International Joint Conference on Automated Reasoning (Springer LNCS 3097, 2004), 372–384.
  55. L. C. Paulson.
    Organizing Numerical Theories Using Axiomatic Type Classes. J. Automated Reasoning 33 1 (2004), 29–49.
    Slides available
  56. Giampaolo Bella, Fabio Massacci and L. C. Paulson.
    An overview of the verification of SET. International J. Information Security 4 (2005), 17–28.
  57. Sidi O. Ehmety and L. C. Paulson.
    Mechanizing Compositional Reasoning for Concurrent Systems: Some Lessons. Formal Aspects of Computing 17 (2005), 58–68.
  58. Tobias Nipkow and L. C. Paulson. Proof Pearl: Defining Functions Over Finite Sets. In: Joe Hurd and Tom Melham (editors),Theorem Proving in Higher Order Logics (Springer LNCS 3603, 2005), 385–396.
  59. L. C. Paulson.
    Defining Functions on Equivalence Classes. ACM Trans. on Computational Logic 7 4 (2006), 658–675.
    Slides available
  60. Giampaolo Bella, Fabio Massacci and L. C. Paulson.
    Verifying the SET Purchase Protocols. J. Automated Reasoning 36 (2006), 5–37.
  61. Jia Meng, Claire Quigley and L. C. Paulson.
    Automation for Interactive Proof: First Prototype. Information and Computation 204 10 (2006), 1575–1596.
  62. Giampaolo Bella and L. C. Paulson.
    Accountability Protocols: Formalized and Verified. ACM Trans. on Information and System Security 9 2 (2006), 138–161.
  63. Jia Meng and L. C. Paulson.
    Lightweight Relevance Filtering for Machine-Generated Resolution Problems. In: Geoff Sutcliffe, Renate Schmidt and Stephan Schulz (editors), ESCoR: Empirically Successful Computerized Reasoning (CEUR Workshop Proceedings, Vol. 192, 2006), 53–69. (See journal version below.)
  64. Jia Meng and L. C. Paulson.
    Translating Higher-Order Problems to First-Order Clauses. In: Geoff Sutcliffe, Renate Schmidt and Stephan Schulz (editors), ESCoR: Empirically Successful Computerized Reasoning (CEUR Workshop Proceedings, Vol. 192, 2006), 70–80.
  65. Behzad Akbarpour and L. C. Paulson.
    Towards Automatic Proofs of Inequalities Involving Elementary Functions. In: Byron Cook and Roberto Sebastiani (editors), PDPAR 2006: Pragmatics of Decision Procedures in Automated Reasoning, 27–37.
  66. Jia Meng, Lawrence C. Paulson and Gerwin Klein
    A Termination Checker for Isabelle Hoare logic. In: Bernhard Beckert (editor), 4th International Verification Workshop, VERIFY’07 (CEUR Workshop Proceedings, Vol. 259, 2007), 104–118.
  67. L. C. Paulson and Kong Woei Susanto.
    Source-level Proof Reconstruction for Interactive Theorem Proving. In: Klaus Schneider and Jens Brandt (editors), Theorem Proving in Higher Order Logics (Springer LNCS 4732, 2007), 232–245.
    Slides available
  68. Behzad Akbarpour and Lawrence C. Paulson.
    Extending a Resolution Prover for Inequalities on Elementary Functions. In: Nachum Dershowitz and Andrei Voronkov (editors), Logic for Programming, Artificial Intelligence, and Reasoning — LPAR 2007 (Springer LNCS 4790), 47–61.
  69. Jia Meng and L. C. Paulson.
    Lightweight Relevance Filtering for Machine-Generated Resolution Problems. J. Applied Logic, in press. Test data available.
  70. Jia Meng and L. C. Paulson.
    Translating higher-order problems to first-order clauses. J. Automated Reasoning 40 1 (2008), 35-60. Test data available.

Last modified 28 January, 2008