Concrete Semantics – A Proof Assistant Approach

This book is two books. Part I is a practical introduction to working with the Isabelle proof assistant. It teaches you how to write functional programs and inductive definitions and how to prove properties about them in Isabelle’s structured proof language. Part II is an introduction to the semantics of imperative languages with an emphasis on applications like compilers and program analysers. The distinguishing features are that every bit of mathematics has been formalized in Isabelle and that much of it is executable. Part I focusses on the details of proofs in Isabelle. Part II can be read even without familiarity with Isabelle’s proof language: all proofs are described in detail but informally. The Isabelle formalization, including the proofs, is available online: all the material, including accompanying slides, can be downloaded from the book’s home page http://www.concrete-semantics.org.

Although the subject matter is semantics and applications, the not-sohidden agenda is to teach the reader two things: the art of precise logical reasoning and the practical use of a proof assistant as a surgical tool for formal proofs about computer science artefacts. In this sense the book represents a formal approach to computer science, not just semantics.

Why?

This book is the marriage of two areas: programming languages and theorem proving. Most programmers feel that they understand the programming language they use and the programs they write. Programming language semantics replaces a warm feeling with precision in the form of mathematical definitions of the meaning of programs. Unfortunately, such definitions are often still at the level of informal mathematics. They are mental tools, but their informal nature, their size, and the amount of detail makes them error prone. Since they are typically written in LATEX, you do not even know whether they would type-check, let alone whether proofs about the semantics, e.g., compiler correctness, are free of bugs such as missing cases.

This is where theorem proving systems (or “proof asistants”) come in, and mathematical (im)precision is replaced by logical certainty. A proof assistant is a software system that supports the construction of mathematical theories as formal language texts that are checked for correctness. The beauty is that this includes checking the logical correctness of all proof text. No more ‘proofs’ that look more like LSD trips than coherent chains of logical arguments. Machine-checked (aka “formal”) proofs offer the degree of certainty required for reliable software but impossible to achieve with informal methods.

In research, the marriage of programming languages and proof assistants has led to remarkable success stories like a verified C compiler and a verified operating system kernel. This book introduces students and professionals to the foundations and applications of this marriage.

Concrete?

• The book shows that a semantics is not a collection of abstract symbols on sheets of paper but formal text that can be checked and executed by the computer: Isabelle is also a programming environment and most of the definitions in the book are executable and can even be exported as programs in a number of (functional) programming languages. For a computer scientist, this is as concrete as it gets.

• Much of the book deals with concrete applications of semantics: compilers, type systems, program analysers.

• The predominant formalism in the book is operational semantics, the most concrete of the various forms of semantics.

• Foundations are made of concrete.