Concrete Semantics with Coq and CoqHammer
Logic in Computer Science
2018-08-21 v1
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.
Keywords
Cite
@article{arxiv.1808.06413,
title = {Concrete Semantics with Coq and CoqHammer},
author = {Łukasz Czajka and Burak Ekici and Cezary Kaliszyk},
journal= {arXiv preprint arXiv:1808.06413},
year = {2018}
}