Concrete semantics (A proof assistant approach)
Se ha publicado un libro de razonamiento formalizado en Isabelle/HOL sobre semántica de lenguajes de programación titulado Concrete semantics (A proof assistant approach).
Sus autores son
- Tobias Nipkow (de la Univ. Técnica de Munich, Alemania) y
- Gerwin Klein (del NICTA, Australia).
Su resumen es
The book Concrete Semantics introduces semantics of programming languages through the medium of a proof assistant. The first part of the book is an introduction to the proof assistant Isabelle. The second part is an introduction to operational semantics and its applications and is based on a simple imperative programming language.
El código de las correspondientes teorías en Isabelle se encuentra aquí.