|
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, capture-avoiding
substitution, etc., is very often a major problem in formal proofs
from the lambda-calculus and programming language theory.
Nominal
Isabelle provides an infrastructure for reasoning conveniently about
bound variables and alpha-equivalence 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_20-Jan-2011/bin/isabelle jedit -l HOL-Nominal2 Minimal.thy
- MacOSX:
nominal_isabelle_20-Jan-2011.app/Isabelle/bin/isabelle jedit -l HOL-Nominal2 Minimal.thy
Windows needs a bit more work explained here. Once done, start Isabelle with
- Windows:
nominal_isabelle_20-Jan-2011/bin/isabelle jedit -l HOL-Nominal2 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 lambda-calculus, 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.
|
