Concrete Semantics: With Isabelle/HOL
by Tobias Nipkow, Gerwin Klein
Publisher: Springer 2016
ISBN/ASIN: 3319105418
Number of pages: 308
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.
Download or read it online for free here:
Download link
(1.6MB, PDF)
Similar books
Introduction to Programming Languages
- Wikibooks
This book is an attempt to describe a bit of the programming languages zoo. We use each of the particular languages to introduce fundamental notions related to the design and the implementation of general purpose programming languages.
(4489 views)
- Wikibooks
This book is an attempt to describe a bit of the programming languages zoo. We use each of the particular languages to introduce fundamental notions related to the design and the implementation of general purpose programming languages.
(4489 views)
Exploring Programming Language Architecture in Perl
by Bill Hails
This book presents an informal and friendly introduction to some of the core ideas in modern computer science, using the programming language Perl as its vehicle. The book takes the form of a series of working interpreters for the language PScheme.
(5483 views)
by Bill Hails
This book presents an informal and friendly introduction to some of the core ideas in modern computer science, using the programming language Perl as its vehicle. The book takes the form of a series of working interpreters for the language PScheme.
(5483 views)
Dictionary of Programming Languages
by Neal Ziring
The Dictionary of Programming Languages is an online compendium of computer coding methods assembled to provide information and aid your appreciation for computer science history. The dictionary currently has over 120 entries.
(7860 views)
by Neal Ziring
The Dictionary of Programming Languages is an online compendium of computer coding methods assembled to provide information and aid your appreciation for computer science history. The dictionary currently has over 120 entries.
(7860 views)
Computational Category Theory
by D.E. Rydeheard, R.M. Burstall
The book is a bridge-building exercise between computer programming and category theory. Basic constructions of category theory are expressed as computer programs. It is a first attempt at connecting the abstract mathematics with concrete programs.
(10835 views)
by D.E. Rydeheard, R.M. Burstall
The book is a bridge-building exercise between computer programming and category theory. Basic constructions of category theory are expressed as computer programs. It is a first attempt at connecting the abstract mathematics with concrete programs.
(10835 views)