jsCoq：迈向混合定理证明界面
编程语言
2017-01-26 v1 人机交互
机器学习
计算机科学中的逻辑
摘要
我们描述 jsCoq，一个用于 Coq 交互式证明辅助工具的新平台和用户环境。jsCoq 系统面向 HTML5-ECMAScript 2015 规范，通常运行在符合标准的浏览器内，无需外部服务器或服务。针对教育用途，jsCoq 因其自包含特性允许用户立即开始与证明脚本交互。实际上，完整的 Coq 环境与证明脚本一起打包，简化了分发和安装。开始使用 jsCoq 就像点击链接一样简单。当前版本附带了 10 多个流行的 Coq 库，并支持流行的书籍如 Software Foundations 或 Certified Programming with Dependent Types。新的目标平台开辟了新的交互和显示可能性。它也促进了某些新的 Coq 相关技术的发展。特别是，我们实现了一种新的基于序列化的与证明辅助工具交互的协议，以及一种新的用于库分发的包格式。
引用
@article{arxiv.1701.07125,
title = {jsCoq: Towards Hybrid Theorem Proving Interfaces},
author = {Emilio Jesús Gallego Arias and Benoît Pin and Pierre Jouvelot},
journal= {arXiv preprint arXiv:1701.07125},
year = {2017}
}
备注
In Proceedings UITP 2016, arXiv:1701.06745