Workshop Papers

(Note: most of these have since been developed into refereed articles.)

  1. L. C. Paulson.
    Inductive analysis of the Internet protocol TLS.
    In: Bruce Christianson, Bruno Crispo, William S. Harbison and Michael Roe (editors), Security Protocols: 6th International Workshop 1998. (Springer LNCS 1550, published 1999), 1–12.
  2. L. C. Paulson.
    Relations between secrets: the Yahalom protocol (extended abstract).
    In: Bruce Christianson, Bruno Crispo, James A. Malcolm and Michael Roe (editors),
    Security Protocols: 7th International Workshop 1999 (Springer LNCS 1550, published 2000), 73–77.
  3. Giampaolo Bella and L. C. Paulson.
    Making sense of specifications: the formalization of SET.
    In    : Bruce Christianson, Bruno Crispo, James A. Malcolm and Michael Roe (editors), Security Protocols: 8th International Workshop 2000. (Springer LNCS 2133, published 2001), 74–81.
  4. Giampaolo Bella and L. C. Paulson.
    A proof of non-repudiation.
    In: Security Protocols: 9th International Workshop     2001. (Springer LNCS 2467, published 2002), 119–125.
  5. Sidi O. Ehmety and L. C. Paulson.
    Representing component states in higher-order logic.
    In    : Richard J. Boulton and Paul B. Jackson (editors),Theorem Proving in Higher Order Logics 2001: Supplemental Proceedings
  6. Christoph Benzmüller, L. C. Paulson, Frank Theiss and Arnaud Fietzke.
    Progress report on Leo-II, an automatic theorem prover for higher-order logic.
    In: Klaus Schneider and Jens Brandt (editors), Theorem Proving in Higher Order Logics 2007 — Emerging Trends.
  7. Jean E. Martina and L. C. Paulson.
    Verifying multicast-based security protocols using the inductive method.
    CryptoForma Workshop 2011: Workshop on Formal Methods and Cryptography, Limerick, June 2011.
  8. Ralph Romanos, L. C. Paulson.
    Proving the impossibility of trisecting an angle and doubling the cube.
    Isabelle Users Workshop (associated with the conference ITP 2012). Princeton, New Jersey, August 2012.
    Isabelle theory development • Slides available
  9. Agnieszka Słowik, Chaitanya Mangla, Mateja Jamnik, Sean Holden and L. C. Paulson.
    Bayesian optimisation for premise selection in automated theorem proving (Student abstract).
    In AAAI Conference on Artificial Intelligence (AAAI 2020). AAAI Press.
  10. L. C. Paulson.
    Ackermann’s function in iterative form: a subtle termination proof with Isabelle/HOL.
    Isabelle Workshop 2020. Slides available • recording available
  11. Yiannos Stathopoulos, Angeliki Koutsoukou-Argyraki and L. C. Paulson.
    SErAPIS: A concept-oriented search engine for the Isabelle libraries based on natural language.
    Isabelle Workshop 2020. Slides available
  12. Chaitanya Mangla, Sean B. Holden and L. C. Paulson. Bayesian optimisation of solver parameters in CBMC. 18th International Workshop on Satisfiability Modulo Theories (SMT), 2020.