-Ware: hardware description and verification in Agda

DOI10.4230/LIPICS.TYPES.2015.9MaRDI QIDQ4580232zbMATH OpenFDO

Authors Flor João Paulo Pizani, Wouter Swierstra, Yorick Sijsling

Publication date 13 August 2018

Full work available at URL https://doi.org/10.4230/LIPICS.TYPES.2015.9

zbMATH Keywords

Agdadependently typed programmingEDSLfunctional programminghardware description languages

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18) Switching theory, applications of Boolean algebras to circuits and networks (94C11)

Recommendations

• Verified timing transformations in synchronous circuits with \(\lambda\pi\)-Ware
• Coquet: a Coq library for verifying hardware
• Certifying circuits in type theory
• A calculus for hardware description
• scientific article; zbMATH DE number 139813

Cites work

• A Brief Overview of Agda – A Functional Language with Dependent Types
• Auto in Agda. Programming proof search using reflection
• Coquet: a Coq library for verifying hardware
• Correct Hardware Design and Verification Methods
• Dependent types and formal synthesis
• FM8501: a verified microprocessor
• Mathematics of Program Construction
• The power of Pi

Cited in

(4)

• Certifying circuits in type theory
• Verified timing transformations in synchronous circuits with \(\lambda\pi\)-Ware
• Coquet: a Coq library for verifying hardware
• Functional Netlists

Describes a project that uses

Uses Software

• Coq
• Haskell
• Coquet
• Lava
• muFP

This page was built for publication: \(\Pi\)-Ware: hardware description and verification in Agda

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