Concrete Semantics with Coq and CoqHammer
Not on the map. Why?
Abstract (arXiv)
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. In order to achieve a similar brevity of the formal text we extensively use CoqHammer, as well as Coq Ltac-level automation. We compare the formalization efficiency, compactness, and the readability of the proof scripts originating from a Coq re-formalization of two chapters from the book.
Key facts. Cited by 2 papers in the map (data through 7 Oct 2026). First posted on arXiv 20 Aug 2018.
Builds on
No reference list yet.
Built on by
Citing papers per year: 2025: 1; 2026: 1.
2 papers.