Concrete Semantics with Isabelle/HOL

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 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 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.

Here are a few good reasons to attend this course:

1. You enjoyed Prof. Smolka's lectures and would like to learn more about interactive theorem proving, program semantics, or both.
2. You missed Prof. Smolka's lectures but would still like to learn about interactive theorem proving, program semantics, or both.
3. You want to develop special skills that will make your Lebenslauf stand out.
4. You want to learn to make puns on the names of proof assistants.
5. You need the credit points.

1. Programming and Proving in Isabelle
2. Case Study: Expressions in a Programming Language
3. Logic and Proof beyond Equality
4. Isar: A Language for Structured Proofs
5. A Small Imperative Language
6. A Compiler
7. Types
8. Program Analysis
9. Denotational Semantics
10. Hoare Logic
11. 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 Isabelle2018. Beware: There are two user interfaces for Isabelle: jEdit and Visual Studio. We assume jEdit in this course.

The official Isabelle documentation

• 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 Main theory.

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 assistant.

Schedule

To avoid collision with the kick-off meeting on 08/04, the lecture starts on Thursday 11/04 instead.

Cancelled lecture dates (holidays): 22/04, 10/06.
Cancelled tutorial dates (other): 10/05, 14/06.

Exercises and Announcements

We will use a moodle to discuss and collect the exercises. You can access it from here.

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 is not yet scheduled.

Contact

You can reach us at sophie.tourret@mpi-inf.mpg.de and mathias.fleury@mpi-inf.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.