CakeMLML语言的验证实施

联合创作 · 2023-09-30 21:37

CakeML是一种具有成熟正确编译器和运行系统的功能性编程语言。

CakeML是基于Standard ML 的重要子集它的语义和编译器算法都强调高阶逻辑,并且已被证明是改造CakeML程序为语义等价的机器代码。

我们使用HOL4的最新开发版本来搭建CakeML,我们在PolyML5.6上创建HOL (http://www.polyml.org)。

示例构建指令可以在build-instructions.sh找到。

浏览 3
点赞
评论
收藏
分享

手机扫一扫分享

编辑 分享
举报
评论
图片
表情
推荐
点赞
评论
收藏
分享

手机扫一扫分享

编辑 分享
举报