Concrete Semantics: With Isabelle/HOL

Concrete Semantics: With Isabelle/HOL

by Tobias Nipkow, Gerwin Klein

eBook Details;

Publisher: Springer 2016
ISBN/ASIN: 3319105418
Number of pages: 308

eBook Description:
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. The distinguishing feature is that all the mathematics has been formalised in Isabelle and much of it is executable.