用于与 Coq 异步交互的 PIDE
人机交互
2014-10-31 v1 计算机科学中的逻辑
摘要
本文描述了将 Coq 证明辅助工具与最初为 Isabelle 开发的 PIDE 架构进行集成的初步进展。该架构旨在实现与证明辅助工具的异步、并行交互，并与一个允许 jEdit 编辑器配合 Isabelle 工作的插件紧密绑定。我们对 PIDE 架构进行了一些泛化，以容纳除 Isabelle 之外的更多证明器，并调整 Coq 以理解核心协议：这在约两个人月的工作量内交付了一个可运行的系统。
引用
@article{arxiv.1410.8221,
title = {PIDE for Asynchronous Interaction with Coq},
author = {Carst Tankink},
journal= {arXiv preprint arXiv:1410.8221},
year = {2014}
}
备注
In Proceedings UITP 2014, arXiv:1410.7850