Papers about Isabelle

[Note: Look elsewhere for Isabelle documentation]

Basic concepts

• L. C. Paulson.
  The foundation of a generic theorem prover. J. Automated Reasoning 5 (1989), 363–397.
• L. C. Paulson.
  Isabelle: the next 700 theorem provers. In: P. Odifreddi (editor), Logic and Computer Science (Academic Press, 1990), 361–386.
• L. C. Paulson.
  Tool support for logics of programs. In: M. Broy (editor), Mathematical Methods in Program Development (Summer School Marktoberdorf 1996), Springer-Verlag, 461–498. Also Report 406, Computer Lab (1996).
  Slides available

On Formalizing Mathematics

• L. C. Paulson.
  Organizing Numerical Theories Using Axiomatic Type Classes. Journal of Automated Reasoning, in press.
  Slides available
• L. C. Paulson.
  Defining Functions on Equivalence Classes. ACM Transactions on Computational Logic, in press.
  Slides available

On the classical reasoner

• 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.
• L. C. Paulson,
  A generic tableau prover and its integration with Isabelle.
  J. Universal Computer Science 5 (3) (1999), 73–87.

Of historical interest

• L. C. Paulson,
  Natural deduction as higher-order resolution. J. Logic Programming 3 (1986), 237–258.
• 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.
• L. C. Paulson,
  A formulation of the simple theory of types (for Isabelle). In: P. Martin-Löf &G. Mints (editors), COLOG-88: International Conf. in Computer Logic.Tallinn, Estonia (1988). Published as Springer LNCS 417, 1990), 246–274.
• L. C. Paulson.
  A preliminary user's manual for Isabelle. Technical Report 133, Computer Lab (1988).
• Tobias Nipkow and L C Paulson,
  Isabelle tutorial and user's manual. Technical Report 189, Computer Lab (1990).
• L. C. Paulson,
  Introduction to Isabelle. Technical Report, Computer Lab (last revised 2003).

Research funded by the EPSRC, projects GR/E0355.7, GR/H40570, and many others.