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 Jean Gallier, Andrew Hicks - University of Pennsylvania
From the table of contents: Automata; Formal Languages (A Grammar for Parsing English, Context-Free Grammars, Derivations and Context-Free Languages, Normal Forms for Context-Free Grammars, Chomsky Normal Form, ...); Computability; Current Topics.
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.
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 Eric C.R. Hehner - Springer
Understanding programming languages requires knowledge of the underlying theoretical model. This book explores aspects of programming that are amenable to mathematical proof. It describes a simple and comprehensive theory.