. Concrete Semantics with Isabelle/HOL

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:  MaterialBackgroundResourcesStudent ProjectsExams and GradesContact


Material


Background

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

  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


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:

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


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.blanchetteSPIDERMONKEYmpi-inf.mpg.de and mathias.fleurySPIDERMONKEYmpi-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, 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