Dr. Jasmin Blanchette
Advanced course at Universität des Saarlandes
6 credit points
Summer semester 2015
Student Projects ⋅
Exams and Grades ⋅
- Main Slides, Java Slides, Subtyping Theory
- Exercise 1: Sheet (28 April 2015), Solutions: Exercises, Homework
- Exercise 2: Sheet (4 May 2015), Solutions: Exercises, Homework
- Exercise 3: Sheet (11 May 2015), Solutions: Exercises, Homework
- Exercise 4: Sheet (18 May 2015), Solutions: Exercises, Homework
- Exercise 5: Sheet (1 June 2015), Solutions: Exercise 1, Exercise 2,
- Exercise 6: Sheet, Template (8 June 2015),
Solutions: Exercise, Homework
- Exercise 7: Sheet (15 June 2015),
Solutions: Exercise 7.1, Exercise 7.2, Homework
- Exercise 8: Sheet, Template (22 June 2015),
Solutions: Exercise 8.1, Exercise 8.2, Homework
- Exercise 9: Sheet, Template (29 June 2015), Solutions: Exercise, Homework
- Exercise 10: Sheet, Template (6 July 2015), Solutions: Exercise
- Exercise 11: Sheet, Template (20 July 2015), Solutions: Exercise, Homework
- Exercise 12: Sheet, Template (27 July 2015), Solutions: Exercise
This course introduces two topics together:
- The first part is a self-contained introduction to the
proof assistant Isabelle/HOL.
- The second part is an introduction to the semantics of imperative
programming languages. This part is formalized in Isabelle.
This advanced course is based on a brand new book by Prof. Tobias Nipkow and Prof. Gerwin Klein, which is
available both as a free PDF online and as a hardcover from Springer. The
material is complementary to the core Semantics course by
Prof. Gert Smolka, which uses
Coq and focuses on the λ-calculus and functional programming.
Proof assistants are tools that allow its users to carry out mathematical
proofs rigorously, based on a logical foundation. Developing a proof in a
proof asssistant as opposed to using pen and paper is roughly the equivalent
of programming on a computer as opposed to sketching pseudocode on paper.
Expertise with proof assistants is becoming an increasingly important skill,
especially for software verification, which aims at proving the
absence of bugs in programs. In the experience of many instructors, the use of
a proof assistant helps students get a good grip on computer science topics.
Coq and Isabelle are the main two proof assistants in use. Isabelle's
strength is that it is simple as 1-2-3: It offers (1) a simple yet
powerful logic, (2) a convenient user interface, and (3) a lot of
There are no formal prerequisites for taking the course. Familiarity with a
typed functional programming language (such as Standard ML, OCaml, Haskell, or
F#), as taught in Programmierung 1, is highly recommended.
|Lectures: ||Monday 10:15 to 11:45, E1 5, 6th floor, Seminarraum
|Tutorials: || Tuesday 10:15 to 11:45, E1 5, 6th floor, Seminarraum
- Programming and Proving in Isabelle
- Case Study: Expressions in a Programming Language
- Logic and Proof beyond Equality
- Isar: A Language for Structured Proofs
- A Small Imperative Language
- A Compiler
- Program Analysis
- Denotational Semantics
- Hoare Logic
- Abstract Interpretation
The Concrete Semantics web
site lists the most important resources for this course. It also includes the
demo files presented in the lectures (e.g., Overview_Demo.thy).
The course is based on Isabelle2014. Beware: There are two user interfaces for
Isabelle: Proof General and jEdit. We assume jEdit in this course. Proof
General support will be discontinued in Isabelle2015, which is expected to be
released in May or June 2015.
more details for those who are curious. In particular:
- prog-prove corresponds roughly to Part~I of the Concrete Semantics book.
- tutorial tells a more comprehensive story. Section 5,
“The Rules of the Game”, is useful if you want to write detailed
proofs, without appealing to sophisticated tactics.
- main is a summary of what's included in the basic
There's a vibrant community around
Isabelle, with mailing lists, wikis, etc.
Higher-order logic (HOL) is a fairly simple (and weak) logic, which we will
learn by doing. Those who are curious and want to know the whole story can
look at the HOL System
LOGIC manual, which is part of the documentation of the HOL4 proof
Overall, 18 formalization projects were submitted by students as answers to
exercise sheet 10. A few of them are collected below, with their authors'
Exams and Grades
Credits and grades will be based on homework (including Isabelle developments)
and a final written exam. The homework counts for 40% of the grade; the exam
The final exam will take place on 10 August 2015 from 14:00 to 16:00 in E1 3,
HS 002. If necessary, a repeat exam is scheduled for 28 September 2015 from
14:00 to 16:00 in E1 5, 6th floor, Seminarraum.
You can reach us at
if you have questions.
Please put [CONCRETE] somewhere in the subject line.
We will also be happy to answer your questions in person, but because the
main instructor is co-located at Inria Nancy, it is a good idea to request
an appointment by email.
“It is blatantly clear”
You stupid machine, that what”
I tell you is true.”
— Michael Norrish”
“Hah! A proof of False.”
Your axioms are bogus.”
Go back to square one.”
— Lawrence C. Paulson”