Prawf: An Interactive Proof System for Program Extraction
Prawf: An Interactive Proof System for Program Extraction
复制标题
DOI：
10.1007/978-3-030-51466-2_12
复制
发表时间：
2020-06-24
期刊：
影响因子：
--
通讯作者：
Tsuiki H
中科院分区：
文献类型：
--
作者：
Berger U;Petrovska O;Tsuiki H
我们提出了一个互动证明系统，该系统专门用于从证明中提取程序。在上一篇论文中，提出了基本理论IFP（直觉固定点逻辑），并证明了其健全性。目前的贡献描述了原型实施，并通过几个案例研究来解释其使用。该系统受益于对理论的改进，这使得可以使用不受限制的严格归纳和共同感应定义从证据中提取程序，从而消除了以前的可接受性限制。
We present an interactive proof system dedicated to program extraction from proofs. In a previous paper the underlying theory IFP (Intuitionistic Fixed Point Logic) was presented and its soundness proven. The present contribution describes a prototype implementation and explains its use through several case studies. The system benefits from an improvement of the theory which makes it possible to extract programs from proofs using unrestricted strictly positive inductive and coinductive definitions, thus removing the previous admissibility restrictions.
影响因子：
1.1
作者：
Tsuiki, H
通讯作者：
Tsuiki, H