Concrete Semantics with Coq and CoqHammer
CICM, pp. 53-59, 2018.
The “Concrete Semantics” book gives an introduction to imperative programming languages accompanied by an Isabelle/HOL formalization. In this paper we discuss a re-formalization of the book using the Coq proof assistant (version 8.7.2). In order to achieve a similar brevity of the formal text we extensively use CoqHammer, as well as Coq L...More
Full Text (Upload PDF)
PPT (Upload PPT)