Concrete Semantics: With Isabelle/HOL

Concrete Semantics: With Isabelle/HOL

by Tobias Nipkow, Gerwin Klein

Paperback(Softcover reprint of the original 1st ed. 2014)

$79.99
View All Available Formats & Editions
Choose Expedited Shipping at checkout for guaranteed delivery by Wednesday, May 1

Product Details

ISBN-13: 9783319357591
Publisher: Springer International Publishing
Publication date: 10/28/2016
Edition description: Softcover reprint of the original 1st ed. 2014
Pages: 298
Product dimensions: 6.10(w) x 9.25(h) x 0.03(d)

About the Author

Prof. Tobias Nipkow received his Ph.D. in Manchester, after which he taught and carried out research at MIT and in Cambridge. He took up a professorship in 1992 at the Technische Universität München where he holds the Chair for Logic and Verification. He was one of the developers of Isabelle, a generic proof assistant, and he coauthored the related LNCS tutorial. He also coauthored the textbook "Term Rewriting and All That", and he is the Editor-in-Chief of the Journal of Automated Reasoning. His research interests include automatic and interactive theorem proving, formal verification, formalizing programming languages, type systems, semantics, rewriting and unification, and the lambda-calculus.

Assoc. Prof. Gerwin Klein received his Ph.D. in Computer Science from the Technische Universität München. He is a Senior Principal Researcher/Research Leader at National ICT Australia (NICTA) and an adjunct professor in the School of Computer Science and Engineering, University of New South Wales. His research interests include interactive theorem proving, software verification, and the semantics of programming languages.

Table of Contents

Introduction.- Programming and Proving.- Case Study: IMP Expressions.- Logic and Proof Beyond Equality.- Isar: A Language for Structured Proofs.- IMP: A Simple Imperative Language.- Compiler.- Types.- Program Analysis.- Denotational Semantics.- Hoare Logic.- Abstract Interpretation.- App. A, Auxiliary Definitions.- App. B, Symbols.- References.

Customer Reviews

Most Helpful Customer Reviews

See All Customer Reviews