Interactive Formal Verification
Principal lecturer: Prof Larry Paulson
Taken by: MPhil ACS
Practical Exercises and the associated Isabelle theory files: replace, powSum, Euclid, semantics
This lecture course introduces interactive formal proof using Isabelle. The lecture notes consist of copies of the slides, some of which have brief remarks attached. Extensive Isabelle documentation is available. The most important single manual is the Tutorial on Isabelle/HOL. Reading the Tutorial is an excellent way of learning Isabelle in depth. However, the Tutorial is a little outdated; although its details remain correct, it presents a style of proof that has become increasingly obsolete with the advent of structured proofs and ever greater automation. These lecture notes take a very different approach and refer you to specific sections of the Tutorial that are particularly appropriate.
Much of the other documentation is only suitable for advanced users. The most useful documents are the Tutorial on Function Definitions, the Tutorial on Type Classes and the Tutorial on Code Generation. The Tutorial on Isar presents a different approach to structured proof than that taken in this course, but the new perspective may be valuable and it is written by the author of Isar.
You can run Isabelle from a Computer Laboratory Linux workstation by typing the following command:
You will probably want to put something in your .profile to shorten this command, either by creating an alias or by augmenting your search path. In order to see special symbols, you need to activate X-symbol mode, as shown. (Unicode tokens works with some installations, but not here.)
Isabelle is easily installed on UNIX based workstations (including Apple Macs), and with greater effort on Windows using Cygwin. Full instructions are available online.
You will also need to learn how to use the text editor Emacs. Advanced skill is not necessary, merely the ability to move backward and forward in a file and to insert or delete text. Learning is not that difficult, especially because the arrow keys and mouse behave more or less as you would expect. A number of Emacs tutorials can be found on the Internet and may be helpful.
Important note: the course sessions take place in three different rooms.
- Mondays at 3 PM in SW01.
- Odd Wednesdays at 11 AM in FW26.
- Even Wednesdays at 11 AM are practical sessions in the terminal room SW02.
There will be no lecture, but Prof Paulson will be available to lend assistance.