Invited Papers, Letters and Other Unrefereed Publications

These include a few early drafts of papers subsequently published later, as well as letters and invited contributions to collected volumes.

  1. L. C. Paulson and Tobias Nipkow. Isabelle Tutorial and User’s Manual. Technical report UCAM-CL-TR-189, Computer Laboratory, University of Cambridge (1990).
  2. L. C. Paulson. Introduction to Isabelle. Technical report UCAM-CL-TR-280, Computer Laboratory, University of Cambridge (1993).
  3. L. C. Paulson. The Isabelle Reference Manual. Technical report UCAM-CL-TR-283, Computer Laboratory, University of Cambridge (1993). Also the 1997 version.
  4. L. C. Paulson. Isabelle’s Object-Logics. Technical report UCAM-CL-TR-286, Computer Laboratory, University of Cambridge (1993). Also the 1997 version.
  5. L. C. Paulson.
    Keep E-Journals Affordable.
    Letter, Communications of the ACM 44 8 (August 2001), 11–13.
  6. L. C. Paulson.
    The Descent of BAN. In: Andrew Herbert and Karen Spärck Jones (editors), Computer Systems: Theory, Technology, and Applications. (Springer, 2004), 225–228.
  7. L. C. Paulson.
    Welcome Defects as a Sign of Innovation?
    Letter, Communications of the ACM 48 11 (November 2005), 11–13.
  8. Markus Wenzel and L. C. Paulson. Isabelle/Isar. In: Freek Wiedijk (editor), The Seventeen Provers of the World (Springer LNCS 3600, 2006), 41–49.
  9. L. C. Paulson.
    Even a Good Abstraction Needs Experience and Testing, Too.
    Letter, Communications of the ACM 50 9 (September 2007), 13–14.
  10. Makarius Wenzel, L. C. Paulson, Tobias Nipkow.
    The Isabelle Framework.
    In: Otmane Ait Mohamed, César Muñoz, Sofiène Tahar (editors),
    Theorem Proving in Higher Order Logics (Springer LNCS 5170, 2008), 33–38.
  11. Christoph Benzmüller and L. C. Paulson.
    Exploring Properties of Normal Multimodal Logics in Simple Type Theory with LEO-II.
    In: Chris Benzmüller, Chad Brown, Jörg Siekmann and Rick Statman (editors), Reasoning in Simple Type Theory: Festschrift in Honor of Peter B. Andrews on His 70th Birthday (College Publications, 2008), 401–422.
  12. Christoph Benzmüller and L.C.Paulson.
    Quantified Multimodal Logics in Simple Type Theory.
    CoRR (2009). Subsequently accepted to Logica Universalis (2012).
  13. L. C. Paulson. Functional Programming in ML.
    In Phillip Laplante (editor), Encyclopedia of Software Engineering (Taylor & Francis, 2010), 333–346.
  14. L. C. Paulson.
    What Liability for Faulty Software?
    Letter, Communications of the ACM 55 2 (February 2012), 6–7.
  15. L. C. Paulson.
    What We Want from Computer Science.
    Letter, Communications of the ACM 56 7 (July 2013), 8–9.
  16. L. C. Paulson.
    Provenance of British Computing.
    Letter, Communications of the ACM 57 9 (September 2014), 8–9.
  17. L. C. Paulson.
    Abolish Software Warranty Disclaimers.
    Letter, Communications of the ACM 58 5 (May 2015), 8–9.
  18. L. C. Paulson.
    Time to Retire 'Computational Thinking'?
    Letter, Communications of the ACM 60 9 (September 2017), 8–9.
  19. L. C. Paulson.
    Predicting Failure of the University.
    Letter, Communications of the ACM 61 4 (April 2018), 8–9.
  20. Jeremy Avigad, Jasmin Christian Blanchette, Gerwin Klein, Lawrence Paulson, Andrei Popescu and Gregor Snelting.
    Introduction to Milestones in Interactive Theorem Proving.
    J. Automated Reasoning 61 1 (2018), 1–8. Publisher's version at www.springerlink.com
  21. Jonas Bayer et al.
    Mathematical Proof Between Generations.
    Notices of the American Mathematical Society (January 2024).