Coquet: A Coq Library for Verifying Hardware
From MaRDI portal
Publication:3100217
DOI10.1007/978-3-642-25379-9_24zbMath1350.68226arXiv1108.4253OpenAlexW1483190703MaRDI QIDQ3100217
Publication date: 22 November 2011
Published in: Certified Programs and Proofs (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1108.4253
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (4)
Modular verification of programs with effects and effects handlers ⋮ Modular verification of programs with effects and effect handlers in Coq ⋮ Unnamed Item ⋮ Functional verification of high performance adders in \textsc{Coq}
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Towards an algebraic theory of Boolean circuits.
- Certifying circuits in type theory
- Proof producing synthesis of arithmetic and cryptographic hardware
- A formally verified compiler back-end
- Geometry of synthesis
- Mathematics of Program Construction
- Theorem Proving in Higher Order Logics
- Higher Order Logic and Hardware Verification
This page was built for publication: Coquet: A Coq Library for Verifying Hardware
