-Ware: hardware description and verification in Agda

DOI10.4230/LIPICS.TYPES.2015.9zbMATH Open1433.68081MaRDI QIDQ4580232FDOQ4580232

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

Publication date: 13 August 2018

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

zbMATH Keywords

functional programmingAgdadependently typed programminghardware description languagesEDSL

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (4)

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

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)