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 (version 8.7.2). 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.
Cite
CITATION STYLE
Czajka, Ł., Ekici, B., & Kaliszyk, C. (2018). Concrete semantics with Coq and CoqHammer. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11006 LNAI, pp. 53–59). Springer Verlag. https://doi.org/10.1007/978-3-319-96812-4_5
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
