Certifying circuits in Type Theory
The work
| Authors | Solange Coupet-Grimal; Line Jakubiec |
|---|---|
| Editors | |
| Type | article |
| Year | 2004 |
| Citekey | coupetgrimal2004certifying |
Where it appeared
| Published in | Formal Aspects of Computing |
|---|---|
| Publisher | Springer Science+Business Media |
| Volume | 16 |
| Issue | 4 |
| Pages | 352--373 |
Identifiers
| DOI | 10.1007/s00165-004-0048-3 |
|---|---|
| OpenAlex | W1996451615 |
Access
| Landing page | https://doi.org/10.1007/s00165-004-0048-3 |
|---|---|
| Free full text | https://dl.acm.org/doi/pdf/10.1007/s00165-004-0048-3 |
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
Abstract We investigate how to take advantage of the particular features of the calculus of inductive constructions in the framework of hardware verification. First, we emphasize in a short case study the use of dependent types and of the constructive aspect of the logic for specifying and synthesizing combinatorial circuits. Then, co-inductive types are introduced to model the temporal aspects of sequential synchronous devices. Moore and Mealy automata are co-inductively axiomatized and are used to represent uniformly both the structures and the behaviors of the circuits. This leads to clear, general and elegant proof processes as is illustrated on the example of a realistic circuit: the ATM Switch Fabric. All the proofs are carried out using Coq.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-26 02:01 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Filed under
Cite it as
@article{coupetgrimal2004certifying,
title = {Certifying circuits in Type Theory},
author = {Solange Coupet-Grimal and Line Jakubiec},
year = {2004},
journal = {Formal Aspects of Computing},
publisher = {Springer Science+Business Media},
volume = {16},
number = {4},
pages = {352--373},
doi = {10.1007/s00165-004-0048-3},
}
This record lives at https://refs.drheap.org/coupetgrimal2004certifying/ and will keep doing so.