Time and Location:
11th August at IJCAR 2008 in
Sydney, Australia.
Download and Installation:
The tutorial will be handson. Please already have Nominal Isabelle installed
before coming to the tutorial. If you have any problems, then do not hesitate
to contact the organisers. The files you need during the tutorial are:
Minimal.thy
Lambda.thy
CK_Machine.thy
Slides
To install Nominal Isabelle you need four packages:
Polyml, Isabelle 2008, an emacs and Proof General:
Download
Installation Notes
Make sure you download the HOLNominal heap file, instead of HOL. If you use
MacOSX and not already use Xemacs, then the easiest method to get Isabelle running
is to use Carbon Emacs and the latest version of Proof General. Ask us for
details.
Once you have Isabelle running make sure XSymbols are switched on
and the HOLNominal heap is loaded.
Overview:
Dealing with binders, renaming of bound variables, captureavoiding
substitution, etc., is very often a major problem in formal proofs
about the lambdacalculus and programming language theory.
Nominal
Isabelle provides an infrastructure for reasoning conveniently about
bound variables and alphaequivalence classes in the proof assistant
Isabelle.
The aim of this tutorial is to give participants a reading
knowledge of nominal techniques and allow them to start using
Nominal Isabelle in their own work.
Programme:
The tutorial will be organised around four sessions:
 08:00  09:00 Help with the installation. If at all possible, already have
Nominal Isabelle installed! See above for instructions.
 09:00  10:00 Session I:
basics, Substitution Lemma, Isar proof language
 10:30  12:30 Session II:
strong induction principles, contexts with holes, betareduction
 14:00  15:30 Session III:
variable convention, evaluation relation
 16:00  17:30 Session IV:
functions, permutations, support
Target audience:
Researchers and doctoral students who want to use Nominal Isabelle to
formalise proofs from the lambdacalculus, from programming language theory or
from proof theory,
such as type soundness, Church Rosser, strong normalisation and so on. The tutorial is
designed for people who have not necessarily used Isabelle or Nominal Isabelle
before, nor
have used any other proof assistant. If you have missed the recent Coqworkshop,
this is your second chance for a tutorial about using a proof assistant.
If you have have been there, the tutorial
will demonstrate an alternative approach to writing POPL papers (see
here for an
example).
Registration: IJCAR webpage
(early registrations deadline: 10 July)
