项目介绍
DeepSpec/dsss17 是一个托管在 GitHub 上的开源项目，主要使用 Coq 编写，目前获得 91 个 Star、15 次 Fork。
- 仓库全名
- DeepSpec/dsss17
README 摘要
dsss17 lecture materials SF local copy of Software Foundations, volumes 1-3 used in Coq Intensive (Pierce) and "Verified functional algorithms" (Appel) CAL materials for "Certifying software with crashes" (Kaashoek / Zeldovich) Stlc materials for "Language specification and variable binding" (Weirich) Metalib support library for Stlc compiler materials for "The structure of a verified compiler" (Leroy) qc materials…
完整内容见 GitHub 原始 README 或本页 。
常见问题
dsss17 用什么语言开发？
主要使用 Coq 编写，目前有 91 个 Star。
如何获取 dsss17 的源码？
可以直接克隆仓库：git clone https://github.com/DeepSpec/dsss17.git，默认分支为 master；安装与运行步骤见仓库 README。
dsss17 最近还在维护吗？
仓库最近一次更新为 2021年9月1日，当前没有未关闭的 Issue；Star 数为 91，可作为社区活跃度的参考。
相关仓库
Kami -一种用于在Coq中设计硬件的数字化用户界面，以及用于证明其正确性的相关语义和定理。Kami的灵感来自Bluespec。它实际上是对麻省理工学院旧版本的完全重写
【原创，已被编入官方教材】Three-level storage subsystem(SD+DDR2 SDRAM+Cache), based on Nexys4 FPGA board. 同济大学计算机系统结构课程设计，FPGA三级存储子系统。
Kirby和Paris的Hydra战斗和Coq中其他有趣数学的变体（协作、记录、包括练习）[maintainer=@Casteran]
de Bruijn语法的自动化和Coq中的替换[maintainers=@RalfJung，@co-dan]
使用 Verilog HDL 在 FPGA 中实现二立方插值
评论