CSCI 7000-000 (1). Current Topics in Computer Science: Practical Theorem Proving with Isabelle/Isar

Jeremy Siek
Spring 2007
Time: Tuesdays, 1pm
Place: ECCR 1B06
Office hours: by appointment, email Jeremy.

Have you ever wanted or needed to prove a property about a formal system but did not know where to start or what techniques to use? Have you ever had trouble sleeping, worrying whether you made a mistake in a paper you just submitted to a conference? If so then this course is for you. The course is a hands-on introduction to theorem proving using the Isabelle proof assistant and the Isar proof language (``Isar'' stands for Intelligible Semi-Automated Reasoning). The course will cover reasoning about inductive datatypes, recursive functions, and sets using propositional, predicate, and higher-order logic (HOL). The course will cover common proof techniques including a cornucopia of induction methods. Last but not least, this course will cover practical issues such as how to ``debug'' your proofs, techniques for structuring large proofs, how to make the best use of Isabelle's decision procedures, and how to get Isabelle to typeset your definitions and proofs in LaTeX. The course has no explicit prerequisites, but a basic understanding of logic is helpful, as is some exposure to functional programming.

I recommend that you bring a laptop computer to class and have a working installation of Isabelle 2005 (see below).

Isabelle resources

The Isabelle web site.
Of particular interest:
Isabelle Software Download
Isabelle/HOL Book
Isar Tutorial
Isar Reference Manual
HOL Reference Manual
The HOL library document: HOL: The basis of Higher-Order Logic.

When using Proof General (an extension of xemacs for interactive Isabelle development), I typically turn on support for x-symbol (menu Proof-General -> Options) and for multiple windows (menu Proof-General -> Options -> Display).

Note for Mac-on-Intel users. Isabelle normally uses polyml for its underlying ML implementation, but polyml has not yet been ported to the Intel macs. Instead you can use SML of NJ. Here's some links to help:

  1. Install SML of NJ
  2. edit Isabelle's settings

Course Notes

All the notes in pdf.