|
Time:
- 9:30 - 11:30, Wednesday, 27 May [slides, Lec1.thy]
- 9:00 - 11:00, Monday, 1 June [slides, Lec2.thy]
- 9:30 - 11:30, Tuesday, 2 June [slides, Lec3.thy,
paper]
The tutorial will take place in Lecture Room 334, State Key Lab of
Computer Science, Level 3 Building #5, Institute of Software, CAS
Download and Installation:
The tutorial will be hands-on. Please already have Isabelle installed on your
laptop before coming to the tutorial. If you do not have a laptop, let us
know. We will find a solution.
If you have any problems with the installation,
then do not hesitate to contact me: urbanc at in tum de. I will also be available
in room 316 at the ISCAS. Please feel free to stop by!
To install Isabelle you need four packages: Polyml, Isabelle 2009, an emacs and
Proof General. Download and Installation instructions for Linux, MacOSX and
Windows are below:
Download
Installation Notes
Once you have Isabelle running make sure XSymbols are switched on (click
on ProofGeneral -> Options -> XSymbols and then save the options).
If you can step through the following theory file, then you are done.
Example.thy
Whenever you have problems, please meet me or send
me an email.
Overview:
The course will be an introduction to the theorem prover Isabelle. No
previous experience with a theorem prover is necessary. During the course
you will be able to follow the examples on your own laptop. I will
start with simple examples about natural numbers and lists. More
advanced examples will come from structural operational semantics. The
hope is that we will be able to prove a compiler correctness theorem
for a WHILE-language. The main aim of the course is to give
participants enough experience to allow them to start using Isabelle in
their own work.
|
|
