Agda 中的 指称硬件设计_设计_文档_相关文件_下载_Agda
介绍
这个 Agda 项目旨在从高级表示规范综合机器验证的并行硬件设计。常见的代数抽象是类别，如从 Haskell 到硬件通过 CCC和向旧程序教授新技巧以及论文编译到类别中所述。
各种表示的语义是通过从操作动机的表示到它们的基本外延的映射给出的。这些映射需要与共享编程接口同态。这个要求产生了一个同态方程的集合，所有这些方程的解都是正确的实现。作为一个令人愉快的副产品，同态还确保所有预期的定律都成立（假设等价是指称的）。
依赖项
Agda 编译器。已知与 Agda 2.6.2 一起使用
Agda 标准库(agda-stdlib)。已知可与 1.7 版一起使用。
Haskell ieee754 软件包（如下面的故障排除所述）
GraphViz用于电路图渲染
建造
Makefile 目标：
compile: 编译模块，但您可以在 Emacs 模式 ( ) 中Test更快地编译。∁-c Cx C-c
tests：在子目录中生成电路图Figures（点文件及其 PDF 效果图）。
更多详情、使用方法，请下载后阅读README.md文件
文件下载
资源详情
[{"title":"（ 71 个子文件 78KB ） Agda 中的 指称硬件设计_设计_文档_相关文件_下载_Agda\n\n","children":[{"title":"denotational-hardware-main","children":[{"title":"Categorical","children":[{"title":"Subcategory.agda <span style='color:#111;'> 7.20KB </span>","children":null,"spread":false},{"title":"MakeLawful.agda <span style='color:#111;'> 2.89KB </span>","children":null,"spread":false},{"title":"Comma","children":[{"title":"Type.agda <span style='color:#111;'> 2.37KB </span>","children":null,"spread":false},{"title":"Raw.agda <span style='color:#111;'> 16.40KB </span>","children":null,"spread":false},{"title":"Homomorphism.agda <span style='color:#111;'> 1.53KB </span>","children":null,"spread":false}],"spread":true},{"title":"Arrow.agda <span style='color:#111;'> 1.96KB </span>","children":null,"spread":false},{"title":"Object.agda <span style='color:#111;'> 1.08KB </span>","children":null,"spread":false},{"title":"Comma.agda <span style='color:#111;'> 1.27KB </span>","children":null,"spread":false},{"title":"Laws.agda <span style='color:#111;'> 11.36KB </span>","children":null,"spread":false},{"title":"Product.agda <span style='color:#111;'> 10.40KB </span>","children":null,"spread":false},{"title":"Free","children":[{"title":"Laws.agda <span style='color:#111;'> 838B </span>","children":null,"spread":false},{"title":"Type.agda <span style='color:#111;'> 563B </span>","children":null,"spread":false},{"title":"Raw.agda <span style='color:#111;'> 699B </span>","children":null,"spread":false},{"title":"Homomorphism.agda <span style='color:#111;'> 2.48KB </span>","children":null,"spread":false}],"spread":true},{"title":"Raw.agda <span style='color:#111;'> 6.47KB </span>","children":null,"spread":false},{"title":"IdInstances.agda <span style='color:#111;'> 1.48KB </span>","children":null,"spread":false},{"title":"Equiv.agda <span style='color:#111;'> 2.50KB </span>","children":null,"spread":false},{"title":"Free.agda <span style='color:#111;'> 533B </span>","children":null,"spread":false},{"title":"Reasoning.agda <span style='color:#111;'> 15.33KB </span>","children":null,"spread":false},{"title":"Homomorphism.agda <span style='color:#111;'> 26.58KB </span>","children":null,"spread":false}],"spread":false},{"title":"SSA.agda <span style='color:#111;'> 2.74KB </span>","children":null,"spread":false},{"title":"Index.agda <span style='color:#111;'> 3.96KB </span>","children":null,"spread":false},{"title":"todo.md <span style='color:#111;'> 56B </span>","children":null,"spread":false},{"title":"Finite","children":[{"title":"Object.agda <span style='color:#111;'> 1.65KB </span>","children":null,"spread":false}],"spread":true},{"title":"Routing.agda <span style='color:#111;'> 182B </span>","children":null,"spread":false},{"title":"Everything.agda <span style='color:#111;'> 709B </span>","children":null,"spread":false},{"title":"Functions","children":[{"title":"Laws.agda <span style='color:#111;'> 2.50KB </span>","children":null,"spread":false},{"title":"Type.agda <span style='color:#111;'> 2.31KB </span>","children":null,"spread":false},{"title":"Raw.agda <span style='color:#111;'> 2.34KB </span>","children":null,"spread":false}],"spread":true},{"title":"Linearize","children":[{"title":"Type.agda <span style='color:#111;'> 1.35KB </span>","children":null,"spread":false},{"title":"Raw.agda <span style='color:#111;'> 3.43KB </span>","children":null,"spread":false},{"title":"Homomorphism.agda <span style='color:#111;'> 12.22KB </span>","children":null,"spread":false}],"spread":true},{"title":"default.nix <span style='color:#111;'> 990B </span>","children":null,"spread":false},{"title":"Primitive","children":[{"title":"Type.agda <span style='color:#111;'> 835B </span>","children":null,"spread":false},{"title":"Raw.agda <span style='color:#111;'> 1.06KB </span>","children":null,"spread":false},{"title":"Homomorphism.agda <span style='color:#111;'> 2.77KB </span>","children":null,"spread":false}],"spread":true},{"title":"Routing","children":[{"title":"Type.agda <span style='color:#111;'> 923B </span>","children":null,"spread":false},{"title":"Raw.agda <span style='color:#111;'> 685B </span>","children":null,"spread":false},{"title":"Homomorphism.agda <span style='color:#111;'> 2.91KB </span>","children":null,"spread":false}],"spread":true},{"title":"readme.md <span style='color:#111;'> 5.24KB </span>","children":null,"spread":false},{"title":"Dot.agda <span style='color:#111;'> 2.57KB </span>","children":null,"spread":false},{"title":".github","children":[{"title":"workflows","children":[{"title":"build-agda.yaml <span style='color:#111;'> 378B </span>","children":null,"spread":false}],"spread":false}],"spread":false},{"title":"Test.agda <span style='color:#111;'> 2.23KB </span>","children":null,"spread":false},{"title":"hardware.agda-lib <span style='color:#111;'> 51B </span>","children":null,"spread":false},{"title":"Primitive.agda <span style='color:#111;'> 495B </span>","children":null,"spread":false},{"title":"Show.agda <span style='color:#111;'> 795B </span>","children":null,"spread":false},{"title":"TFinite.agda <span style='color:#111;'> 3.83KB </span>","children":null,"spread":false},{"title":"Equality.agda <span style='color:#111;'> 150B </span>","children":null,"spread":false},{"title":"Examples","children":[{"title":"Add.agda <span style='color:#111;'> 2.64KB </span>","children":null,"spread":false},{"title":"Conv.agda <span style='color:#111;'> 3.01KB </span>","children":null,"spread":false},{"title":"Add","children":[{"title":"Properties.agda <span style='color:#111;'> 3.35KB </span>","children":null,"spread":false}],"spread":false}],"spread":false},{"title":"Finite.agda <span style='color:#111;'> 463B </span>","children":null,"spread":false},{"title":"Equality","children":[{"title":"Laws.agda <span style='color:#111;'> 397B </span>","children":null,"spread":false},{"title":"Type.agda <span style='color:#111;'> 191B </span>","children":null,"spread":false},{"title":"Raw.agda <span style='color:#111;'> 536B </span>","children":null,"spread":false},{"title":"Homomorphism.agda <span style='color:#111;'> 772B </span>","children":null,"spread":false}],"spread":false},{"title":"Linearize.agda <span style='color:#111;'> 174B </span>","children":null,"spread":false},{"title":"StronglyFinite.agda <span style='color:#111;'> 9.69KB </span>","children":null,"spread":false},{"title":".gitignore <span style='color:#111;'> 110B </span>","children":null,"spread":false},{"title":"HasAlgebra.agda <span style='color:#111;'> 5.94KB </span>","children":null,"spread":false},{"title":"Ty","children":[{"title":"Utils.agda <span style='color:#111;'> 1.17KB </span>","children":null,"spread":false}],"spread":false},{"title":"Makefile <span style='color:#111;'> 465B </span>","children":null,"spread":false},{"title":"Figures","children":[{"title":"Makefile <span style='color:#111;'> 632B </span>","children":null,"spread":false}],"spread":false},{"title":"Old","children":[{"title":"Finite","children":[{"title":"Laws.agda <span style='color:#111;'> 509B </span>","children":null,"spread":false},{"title":"Fun.agda <span style='color:#111;'> 4.10KB </span>","children":null,"spread":false},{"title":"Type.agda <span style='color:#111;'> 321B </span>","children":null,"spread":false},{"title":"Raw.agda <span style='color:#111;'> 1.32KB </span>","children":null,"spread":false},{"title":"Homomorphism.agda <span style='color:#111;'> 1.59KB </span>","children":null,"spread":false}],"spread":false},{"title":"Finite.agda <span style='color:#111;'> 148B </span>","children":null,"spread":false}],"spread":false},{"title":"Functions.agda <span style='color:#111;'> 145B </span>","children":null,"spread":false},{"title":"Ty.agda <span style='color:#111;'> 3.88KB </span>","children":null,"spread":false}],"spread":false}],"spread":true}]
评论信息
其他资源
- 山东大学数字图像处理实验四：图像滤波
- 天眼查.py自动下载企业信用报告
- build-tool 25.0.3 dx.jar
- 《Android移动应用开发案例教程》项目源代码
- 带回声消除功能的Windows Core Audio（MMDeviceApi）音频采集
- 电影数据库xml格式
- 高频电子线路第五版 张肃文
- 杭电面向对象课程本科研究生期末考试试卷，有uml,设计模式大概十五套卷子
- Clojure高级编程 [（美）Jeremy Anderson著]
- vmware开启esxi并做共享磁盘（模拟存储）
- ReportEidolon使用帮助
- 基于ASP.NET的课程管理系统
- Verilog HDL实现了使用WM8731对音频进行采样，并且使用ALTERA FPGA实现了频谱计算（FFT），在VGA上显示频谱
- 编码光栅滤波及其应用
- Bochs-win64-2.6.11.zip
- terraform-kubestack：Terraform GitOps框架—在一个免费的开源框架中为AKS，EKS和GKE Kubernetes集群构建可靠的自动化所需的一切-源码
- 图书管理系统+Java源代码+SQL Server数据库文件
- AGV双路径运行系统及其实现方法
- HprSnap6 6.13.2.0 汉化破解绿色版本
- 学生选课系统软件工程报告文档
- 雷达信号处理基础part1
免责申明
【只为小站】的资源来自网友分享，仅供学习研究，请务必在下载后24小时内给予删除，不得用于其他任何用途，否则后果自负。基于互联网的特殊性，【只为小站】 无法对用户传输的作品、信息、内容的权属或合法性、合规性、真实性、科学性、完整权、有效性等进行实质审查；无论 【只为小站】 经营者是否已进行审查，用户均应自行承担因其传输的作品、信息、内容而可能或已经产生的侵权或权属纠纷等法律责任。
本站所有资源不代表本站的观点或立场，基于网友分享，根据中国法律《信息网络传播权保护条例》第二十二条之规定，若资源存在侵权或相关问题请联系本站客服人员，zhiweidada#qq.com，请把#换成@，本站将给予最大的支持与配合，做到及时反馈和处理。关于更多版权及免责申明参见 版权及免责申明
本站所有资源不代表本站的观点或立场，基于网友分享，根据中国法律《信息网络传播权保护条例》第二十二条之规定，若资源存在侵权或相关问题请联系本站客服人员，zhiweidada#qq.com，请把#换成@，本站将给予最大的支持与配合，做到及时反馈和处理。关于更多版权及免责申明参见 版权及免责申明