-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

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)

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)

• 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)