Towards a Coq-verified Chain of Esterel Semantics
The work
| Authors | Lionel Rieg; Gérard Berry |
|---|---|
| Editors | |
| Type | article |
| Year | 2019 |
| Citekey | rieg2019coqverified |
Where it appeared
| Published in | HAL |
|---|---|
| Publisher | Centre pour la Communication Scientifique Directe |
| Volume | 10 |
| Issue | 1 |
Identifiers
| arXiv | 1909.12582 from its oa_pdf_url |
|---|---|
| DOI | 10.4230/lites.10.1.2 |
| OpenAlex | W4320350427 |
Access
| Landing page | https://hal.science/hal-05288996 |
|---|---|
| Free full text | http://arxiv.org/pdf/1909.12582 |
From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.
Abstract
This article focuses on formally specifying and verifying the chain of formal semantics of the Esterel synchronous programming language using the Coq proof assistant. In particular, in addition to the standard logical (LBS) semantics, constructive semantics (CBS) and constructive state semantics (CSS), we introduce a novel microstep semantics that gets rid of the Must/Can potential function pair of the constructive semantics and can be viewed as an abstract version of Esterel’s circuit semantics used by compilers to generate software code and hardware designs. The article also comes with formal proofs in Coq of the equivalence between the CBS and CSS semantics and of the refinement of the CSS by the microstep semantics, except for the loop construct of Esterel.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-25 20:08 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Cite it as
@article{rieg2019coqverified,
title = {Towards a Coq-verified Chain of Esterel Semantics},
author = {Lionel Rieg and Gérard Berry},
year = {2019},
journal = {HAL},
publisher = {Centre pour la Communication Scientifique Directe},
volume = {10},
number = {1},
doi = {10.4230/lites.10.1.2},
}
This record lives at https://refs.drheap.org/rieg2019coqverified/ and will keep doing so.