Recognition: unknown
Concrete Semantics with Coq and CoqHammer
classification
💻 cs.LO
keywords
bookconcretecoqhammerformalizationproofre-formalizationsemanticsaccompanied
read the original abstract
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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.