Tobias Nipkow

This book is an introduction to data structures and algorithms for functional programming languages, with a focus on proofs. Starting with sorting and searching, it moves on to priority queues and advanced design and analysis techniques: dynamic programming, amortized analysis, splay trees, skew heaps and pairing heaps. The final part of the book covers a number of selected fun topics: graph algorithms, string search, Huffman's algorithm for generating optimal codes and alpha-beta pruning of game trees. The book covers both correctness (does the algorithm do what it is supposed to do?) and running time analysis (does the algorithm terminate within a specified number of steps?). It does so in a unified manner with inductive proofs about functional programs and their running time functions. What sets this book apart from existing books on algorithms is that all proofs have been machine-checked, by the proof assistant Isabelle. That is, in addition to the text in the book, which requires no knowledge of proof assistants!, the Isabelle definitions and proofs are available online. The structured nature of Isabelle proofs permits even novices to follow the high-level arguments. This book is aimed at teachers and students (it has been classroom-tested for a number of years) but is also a reference work for programmers and researchers who are interested in the (verified!) details of some algorithm or proof.

This book is an introduction to data structures and algorithms for functional programming languages, with a focus on proofs. Starting with sorting and searching, it moves on to priority queues and advanced design and analysis techniques: dynamic programming, amortized analysis, splay trees, skew heaps and pairing heaps. The final part of the book covers a number of selected fun topics: graph algorithms, string search, Huffman's algorithm for generating optimal codes and alpha-beta pruning of game trees. The book covers both correctness (does the algorithm do what it is supposed to do?) and running time analysis (does the algorithm terminate within a specified number of steps?). It does so in a unified manner with inductive proofs about functional programs and their running time functions. What sets this book apart from existing books on algorithms is that all proofs have been machine-checked, by the proof assistant Isabelle. That is, in addition to the text in the book, which requires no knowledge of proof assistants!, the Isabelle definitions and proofs are available online. The structured nature of Isabelle proofs permits even novices to follow the high-level arguments. This book is aimed at teachers and students (it has been classroom-tested for a number of years) but is also a reference work for programmers and researchers who are interested in the (verified!) details of some algorithm or proof.

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.

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.

This volume is a self-contained introduction to interactive proof in high- order logic (HOL), using the proof assistant Isabelle 2002. Compared with existing Isabelle documentation, it provides a direct route into higher-order logic, which most people prefer these days. It bypasses ?rst-order logic and minimizes discussion of meta-theory. It is written for potential users rather than for our colleagues in the research world. Another departure from previous documentation is that we describe Markus Wenzel’s proof script notation instead of ML tactic scripts. The l- ter make it easier to introduce new tactics on the ?y, but hardly anybody does that. Wenzel’s dedicated syntax is elegant, replacing for example eight simpli?cation tactics with a single method, namely simp, with associated - tions. The book has three parts. – The ?rst part, Elementary Techniques, shows how to model functional programs in higher-order logic. Early examples involve lists and the natural numbers. Most proofs are two steps long, consisting of induction on a chosen variable followed by the auto tactic. But even this elementary part covers such advanced topics as nested and mutual recursion. – The second part, Logic and Sets, presents a collection of lower-level tactics that you can use to apply rules selectively. It also describes I- belle/HOL’s treatment of sets, functions, and relations and explains how to de?ne sets inductively. One of the examples concerns the theory of model checking, and another is drawn from a classic textbook on formal languages.