Concrete Semantics with Coq and CoqHammer

Łukasz Czajka, Burak Ekici and Cezary Kaliszyk

11th Conference on Intelligent Computer Mathematics (CICM 2018), Springer LNAI 11006, 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 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.


  PDF |    doi:10.1007/978-3-319-96812-4_5  |  © Springer International Publishing AG, part of Springer Nature 2018


author = "\L ukasz Czajka, Burak Ekici and Cezary Kaliszyk",
title = "Concrete Semantics with Coq and CoqHammer",
booktitle = "Intelligent Computer Mathematics - 11th International Conference, {CICM} 2018,
Hagenberg, Austria, August 13-17, 2018, Proceedings",
editor = "Florian Rabe, William M. Farmer, Grant O. Passmore and Abdou Youssef",
series = "Lecture Notes in Computer Science",
volume = "11006",
pages = "53--59",
year = "2018",
url = "",
doi = "10.1007/978-3-319-96812-4_5"
Nach oben scrollen