TL;DR
This paper presents a Coq-based formalization of the 'Concrete Semantics' book, leveraging CoqHammer and Ltac automation to improve efficiency, compactness, and readability of proofs compared to the original Isabelle/HOL version.
Contribution
It introduces a Coq re-formalization of the book's semantics, utilizing advanced automation tools to enhance proof development and readability.
Findings
Coq formalization is comparable in efficiency to Isabelle/HOL
Proof scripts are more compact and readable in Coq
Automation tools significantly reduce proof development effort
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
