Concrete Semantics: With Isabelle/HOL
by Tobias Nipkow, Gerwin Klein
Publisher: Springer 2016
Number of pages: 308
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.
Home page url
Download or read it online for free here:
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.
by Alexander Stepanov, Paul McJones - Semigroup Press
This book applies the deductive method to programming by affiliating programs with the abstract mathematical theories. Specification of these theories, algorithms and theorems and lemmas describing their properties are presented together.
by Robert Harper
Provides an account of the role of type theory in programming language design and implementation. The stress is on the use of types as a tool for analyzing programming language features and studying their implementation.
by Noah D. Goodman, Andreas Stuhlmüller - dippl.org