Time and Location:
23rd January at POPL 2011 in
Austin, USA.
Lambda.thy
Tutorial1.thy
Tutorial2.thy
Tutorial3.thy
Tutorial4.thy
Tutorial5.thy
Tutorial6.thy
Overview:
Dealing with binders, renaming of bound variables, captureavoiding
substitution, etc., is very often a major problem in formal proofs
from 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 below for instructions.
 09:00  10:30 Session I
 11:00  12:30 Session II
 12:30  14:00 Lunch (in hotel)
 14:00  15:30 Session III
 16:00  17:30 Session IV
Download and Installation:
For the tutorial, you need to install one of the following bundles:
For Linux and MacOSX, just unpack them and start Isabelle by typing on the command line:
 Linux:
nominal_isabelle_20Jan2011/bin/isabelle jedit l HOLNominal2 Minimal.thy
 MacOSX:
nominal_isabelle_20Jan2011.app/Isabelle/bin/isabelle jedit l HOLNominal2 Minimal.thy
Windows needs a bit more work explained here. Once done, start Isabelle with
 Windows:
nominal_isabelle_20Jan2011/bin/isabelle jedit l HOLNominal2 Minimal.thy
A testfile is Minimal.thy.
Further installation instructions and minimal requirements are here. You are done, if you see a window like
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.
