
Concrete Semantics with Isabelle/HOL
Dr. Jasmin Blanchette
Mathias Fleury
Daniel Wand
Advanced course at Universität des Saarlandes
6 credit points
Summer semester 2015
Contents:
Material ⋅
Background ⋅
Resources ⋅
Student Projects ⋅
Exams and Grades ⋅
Contact
Material
 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,
Homework
 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
Background
This course introduces two topics together:
 The first part is a selfcontained 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 123: It offers (1) a simple yet
powerful logic, (2) a convenient user interface, and (3) a lot of
proof automation.
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

Topics:
 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
 Types
 Program Analysis
 Denotational Semantics
 Hoare Logic
 Abstract Interpretation
Resources
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.
The official
Isabelle documentation
more details for those who are curious. In particular:
 progprove 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
Main theory.
There's a vibrant community around
Isabelle, with mailing lists, wikis, etc.
Higherorder 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
assistant.
Student Projects
Overall, 18 formalization projects were submitted by students as answers to
exercise sheet 10. A few of them are collected below, with their authors'
permission.
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
for 60%.
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.
Contact
You can reach us at
jasmin.blanchetteSPIDERMONKEYmpiinf.mpg.de and
mathias.fleurySPIDERMONKEYmpiinf.mpg.de
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 colocated 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”
