Certifying circuits in type theory

DOI10.1007/S00165-004-0048-3MaRDI QIDQ1764432zbMATH OpenOpenAlexFDO

Authors Solange Coupet-Grimal, Line Jakubiec

Publication date 24 February 2005

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00165-004-0048-3

zbMATH Keywords

Co-inductionDependent typesExtractionFormal methodsHardware verificationType theory

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Recommendations

• Coquet: a Coq library for verifying hardware
• Circuits as streams in Coq: verification of a sequential multiplier
• -Ware: hardware description and verification in Agda
• Verified timing transformations in synchronous circuits with \(\lambda\pi\)-Ware
• Using an induction prover for verifying arithmetic circuits

Cited in

(12)

• Verified timing transformations in synchronous circuits with \(\lambda\pi\)-Ware
• Functional verification of high performance adders in \textsc{Coq}
• Certifying term rewriting proofs in ELAN
• Coquet: a Coq library for verifying hardware
• scientific article; zbMATH DE number 1163991 (Why is no real title available?)
• scientific article; zbMATH DE number 1500559 (Why is no real title available?)
• -Ware: hardware description and verification in Agda
• An application of co-inductive types in Coq: verification of the alternating bit protocol
• Circuits as streams in Coq: verification of a sequential multiplier
• Verifiable certificates for predicate subtyping
• Coq and hardware verification: a case study
• ``Backward coinduction, Nash equilibrium and the rationality of escalation

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Certifying circuits in type theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1764432)