Concrete Semantics with Coq and CoqHammer

CICM, pp. 53-59, 2018.

Cited by: 0|Bibtex|Views2|Links
EI

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 L...More

Code:

Data:

Your rating :
0

 

Tags
Comments