介绍 这个 Agda 项目旨在从高级表示规范综合机器验证的并行硬件设计。常见的代数抽象是类别，如从 Haskell 到硬件通过 CCC和向旧程序教授新技巧以及论文编译到类别中所述。 各种表示的语义是通过从操作动机的表示到它们的基本外延的映射给出的。这些映射需要与共享编程接口同态。这个要求产生了一个同态方程的集合，所有这些方程的解都是正确的实现。作为一个令人愉快的副产品，同态还确保所有预期的定律都成立（假设等价是指称的）。 依赖项 Agda 编译器。已知与 Agda 2.6.2 一起使用 Agda 标准库(agda-stdlib)。已知可与 1.7 版一起使用。 Haskell ieee754 软件包（如下面的故障排除所述） GraphViz用于电路图渲染 建造 Makefile 目标： compile: 编译模块，但您可以在 Emacs 模式 ( ) 中Test更快地编译。∁-c C­x C-c tests：在子目录中生成电路图Figures（点文件及其 PDF 效果图）。 更多详情、使用方法，请下载后阅读README.md文件

Agda 中的免费应用程序 有关生成的文档，请参阅