Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top

2014 | Book

Introduction Read chapter Read first chapter

Concrete Semantics

With Isabelle/HOL

Authors: Tobias Nipkow, Gerwin Klein

Publisher: Springer International Publishing

Part of: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Login to get access
insite
SEARCH

About this book

Part I of this book 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 feature is that all the mathematics has been formalised in Isabelle and 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 book teaches the reader 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 it represents a formal approach to computer science, not just semantics. The Isabelle formalisation, including the proofs and accompanying slides, are freely available online, and the book is suitable for graduate students, advanced undergraduate students, and researchers in theoretical computer science and logic.

Table of Contents

Frontmatter

Isabelle

Frontmatter
Chapter 1. Introduction
Abstract
Isabelle is a generic system for implementing logical formalisms, and Isabelle/HOL is the specialization of Isabelle for HOL, which abbreviates Higher-Order Logic. We introduce HOL step by step following the equation.
Tobias Nipkow, Gerwin Klein
Chapter 2. Programming and Proving
Abstract
This chapter introduces HOL as a functional programming language and shows how to prove properties of functional programs by induction.
Tobias Nipkow, Gerwin Klein
Chapter 3. Case Study: IMP Expressions
Abstract
The methods of the previous chapter suffice to define the arithmetic and Boolean expressions of the programming language IMP that is the subject of this book. In this chapter we define their syntax and semantics, write little optimizers for them and show how to compile arithmetic expressions to a simple stack machine. Of course we also prove the correctness of the optimizers and compiler!
Tobias Nipkow, Gerwin Klein
Chapter 4. Logic and Proof Beyond Equality
Abstract
The core syntax of formulas (form below) provides the standard logical constructs, in decreasing order of precedence.
Tobias Nipkow, Gerwin Klein
Chapter 5. Isar: a Language for Structured Proofs
Abstract
Apply-scripts are unreadable and hard to maintain. The language of choice for larger proofs is Isar. The two key features of Isar are (1) It is structured, not linear. (2) It is readable without its being run because you need to state what you are proving at any given point. Whereas apply-scripts are like assembly language programs, Isar proofs are like structured programs with comments. A typical Isar proof looks like this.
Tobias Nipkow, Gerwin Klein

Semantics

Frontmatter
Chapter 6. Programming and Proving
Abstract
This chapter introduces HOL as a functional programming language and shows how to prove properties of functional programs by induction.
Tobias Nipkow, Gerwin Klein
Chapter 7. IMP: A Simple Imperative Language
Abstract
To talk about semantics, we first need a programming language. This chapter defines one: a minimalistic imperative programming language called IMP. The main aim of this chapter is to introduce the concepts of commands and their abstract syntax, and to use them to illustrate two styles of defining the semantics of a programming language: big-step and small-step operational semantics. Our first larger theorem about IMP will be the equivalence of these two definitions of its semantics. As a smaller concrete example, we will apply our semantics to the concept of program equivalence.
Tobias Nipkow, Gerwin Klein
Chapter 8. Compiler
Abstract
This chapter presents a first application of programming language semantics: proving compiler correctness. To this end, we will define a small machine language based on a simple stack machine. Stack machines are common lowlevel intermediate languages; the Java Virtual Machine is one example. We then write a compiler from IMP to this language and prove that the compiled program has the same semantics as the source program. The compiler will perform a very simple standard optimization for boolean expressions, but is otherwise non-optimizing.
Tobias Nipkow, Gerwin Klein
Chapter 9. Types
Abstract
This chapter introduces types into IMP, first a traditional programming language type system, then more sophisticated type systems for information flow analysis. Why bother with types? Because they prevent mistakes. They are a simple, automatic way to find obvious problems in programs before these programs are ever run.
Tobias Nipkow, Gerwin Klein
Chapter 10. Program Analysis
Abstract
Program analysis, also known as static analysis, describes a whole field of techniques for the static (i.e. compile-time) analysis of programs.
Tobias Nipkow, Gerwin Klein
Chapter 11. Denotational Semantics
Abstract
So far we have worked exclusively with various operational semantics which are defined by inference rules that tell us how to execute some command. But those rules do not tell us directly what the meaning of a command is. This is what denotational semantics is about: mapping syntactic objects to their denotation or meaning. In fact, we are already familiar with two examples, namely the evaluation of arithmetic and boolean expressions.
Tobias Nipkow, Gerwin Klein
Chapter 12. Hoare Logic
Abstract
So far we have proved properties of IMP, like type soundness, or properties of tools for IMP, like compiler correctness, but almost never properties of individual IMP programs. The Isabelle part of the book has taught us how to prove properties of functional programs, but not of imperative ones.
Tobias Nipkow, Gerwin Klein
Chapter 13. Abstract Interpretation
Abstract
In Chapter 10 we saw a number of automatic program analyses, and each one was hand crafted. Abstract Interpretation is a generic approach to automatic program analysis. In principle, it covers all of our earlier analyses. In this chapter we ignore the optimizing program transformations that accompany certain analyses.
Tobias Nipkow, Gerwin Klein
Backmatter
Metadata
Title
Concrete Semantics
Authors
Tobias Nipkow
Gerwin Klein
Copyright Year
2014
Electronic ISBN
978-3-319-10542-0
Print ISBN
978-3-319-10541-3
DOI
https://doi.org/10.1007/978-3-319-10542-0

Premium Partner

    Image Credits