Reseña: “Concrete semantics” with Coq and CoqHammer
Se ha publicado un artículo de razonamiento formalizado en Coq titulado “Concrete semantics” with Coq and CoqHammer.
Sus autores son
- Łukasz Czajka (de la Universidad de Copenhagen),
- Burak Ekici (de la Universidad de Innsbruck) y
- Cezary Kaliszyk (de la Universidad de Innsbruck).
Su resumen es
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.
El trabajo se ha presentado el 15 de agosto en el CICM 2018 (11th Conference on Intelligent Computer Mathematics).
El código de las correspondientes teorías se encuentra en GitHub.