Concrete Semantics with Coq and CoqHammer

Łukasz Czajka; Burak Ekici; Cezary Kaliszyk

doi:10.1007/978-3-319-96812-4_5

Concrete Semantics with Coq and CoqHammer

Łukasz Czajka, Burak Ekici, Cezary Kaliszyk

Department of Computer Science

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.

Original language	English
Title of host publication	Intelligent Computer Mathematics : 11th International Conference, CICM 2018 Hagenberg, Austria, August 13–17, 2018 Proceedings
Editors	Florian Rabe, William M. Farmer, Grant O. Passmore, Abdou Youssef
Publisher	Springer
Publication date	18 Jul 2018
Pages	53-59
Article number	5
ISBN (Print)	978-3-319-96811-7
ISBN (Electronic)	978-3-319-96812-4
DOIs	https://doi.org/10.1007/978-3-319-96812-4_5
Publication status	Published - 18 Jul 2018
Event	11th International Conference on Intelligent Computer Mathematic - Hagenberg, Austria Duration: 13 Aug 2018 → 17 Aug 2018

Conference

Conference	11th International Conference on Intelligent Computer Mathematic
Country/Territory	Austria
City	Hagenberg
Period	13/08/2018 → 17/08/2018

Series	Lecture Notes in Computer Science
Volume	11006
ISSN	0302-9743

Access to Document

10.1007/978-3-319-96812-4_5

Cite this

Czajka, Ł., Ekici, B., & Kaliszyk, C. (2018). Concrete Semantics with Coq and CoqHammer. In F. Rabe, W. M. Farmer, G. O. Passmore, & A. Youssef (Eds.), Intelligent Computer Mathematics: 11th International Conference, CICM 2018 Hagenberg, Austria, August 13–17, 2018 Proceedings (pp. 53-59). [5] Springer. Lecture Notes in Computer Science Vol. 11006 https://doi.org/10.1007/978-3-319-96812-4_5

Concrete Semantics with Coq and CoqHammer. / Czajka, Łukasz; Ekici, Burak; Kaliszyk, Cezary.

Intelligent Computer Mathematics: 11th International Conference, CICM 2018 Hagenberg, Austria, August 13–17, 2018 Proceedings. ed. / Florian Rabe; William M. Farmer; Grant O. Passmore; Abdou Youssef. Springer, 2018. p. 53-59 5 (Lecture Notes in Computer Science, Vol. 11006).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Czajka, Ł, Ekici, B & Kaliszyk, C 2018, Concrete Semantics with Coq and CoqHammer. in F Rabe, WM Farmer, GO Passmore & A Youssef (eds), Intelligent Computer Mathematics: 11th International Conference, CICM 2018 Hagenberg, Austria, August 13–17, 2018 Proceedings., 5, Springer, Lecture Notes in Computer Science, vol. 11006, pp. 53-59, 11th International Conference on Intelligent Computer Mathematic, Hagenberg, Austria, 13/08/2018. https://doi.org/10.1007/978-3-319-96812-4_5

Czajka Ł, Ekici B, Kaliszyk C. Concrete Semantics with Coq and CoqHammer. In Rabe F, Farmer WM, Passmore GO, Youssef A, editors, Intelligent Computer Mathematics: 11th International Conference, CICM 2018 Hagenberg, Austria, August 13–17, 2018 Proceedings. Springer. 2018. p. 53-59. 5. (Lecture Notes in Computer Science, Vol. 11006). doi: 10.1007/978-3-319-96812-4_5

Czajka, Łukasz ; Ekici, Burak ; Kaliszyk, Cezary. / Concrete Semantics with Coq and CoqHammer. Intelligent Computer Mathematics: 11th International Conference, CICM 2018 Hagenberg, Austria, August 13–17, 2018 Proceedings. editor / Florian Rabe ; William M. Farmer ; Grant O. Passmore ; Abdou Youssef. Springer, 2018. pp. 53-59 (Lecture Notes in Computer Science, Vol. 11006).

@inproceedings{e871859f40a84000906ce302bacf1ee8,

title = "Concrete Semantics with Coq and CoqHammer",

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.",

author = "{\L}ukasz Czajka and Burak Ekici and Cezary Kaliszyk",

year = "2018",

month = jul,

day = "18",

doi = "10.1007/978-3-319-96812-4_5",

language = "English",

isbn = "978-3-319-96811-7",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "53--59",

editor = "Rabe, {Florian } and Farmer, {William M. } and Passmore, {Grant O. } and Youssef, {Abdou }",

booktitle = "Intelligent Computer Mathematics",

note = "11th International Conference on Intelligent Computer Mathematic ; Conference date: 13-08-2018 Through 17-08-2018",

}

TY - GEN

T1 - Concrete Semantics with Coq and CoqHammer

AU - Czajka, Łukasz

AU - Ekici, Burak

AU - Kaliszyk, Cezary

PY - 2018/7/18

Y1 - 2018/7/18

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-319-96812-4_5

DO - 10.1007/978-3-319-96812-4_5

M3 - Article in proceedings

SN - 978-3-319-96811-7

T3 - Lecture Notes in Computer Science

SP - 53

EP - 59

BT - Intelligent Computer Mathematics

A2 - Rabe, Florian

A2 - Farmer, William M.

A2 - Passmore, Grant O.

A2 - Youssef, Abdou

PB - Springer

T2 - 11th International Conference on Intelligent Computer Mathematic

Y2 - 13 August 2018 through 17 August 2018

ER -

Concrete Semantics with Coq and CoqHammer

Abstract

Conference

Access to Document

Fingerprint

Cite this