Towards Certified Meta-Programming with Typed Template-Coq
Towards Certified Meta-Programming with Typed Template-Coq
复制标题
DOI：
10.1007/978-3-319-94821-8_2
复制
发表时间：
2018-07
期刊：
影响因子：
--
通讯作者：
A. Anand;S. Boulier;C. Cohen;Matthieu Sozeau;Nicolas Tabareau
中科院分区：
文献类型：
--
作者：
A. Anand;S. Boulier;C. Cohen;Matthieu Sozeau;Nicolas Tabareau
模板-Coq（ https://template-coq.github.io/template-coq ）是一个Coq的插件，最初由Malecha实现[18]，它提供了Coq术语和全局声明的具体化，如Coq内核所示，以及一个denotation命令。最初，它是为了在Gallina的Coq AST上编写函数而开发的。最近，它被用于CertiCoq认证的编译器项目[4]，作为其前端语言，用于导出参数属性[3]，并将Coq项提取到CBV演算[13]。然而，语法缺乏语义，无论是类型语义还是操作语义，都应该反映Coq的类型理论本身的语义，作为Coq中的正式规范。该工具也相当简单，只提供基本的引用和取消引用命令。我们将其推广到处理整个归纳构造演算（CIC），由Coq实现，包括定义和归纳的内核声明结构，并实现一个Monad用于Coq逻辑环境的一般操作。我们演示了这种设置如何允许Coq用户定义多种通用插件，其正确性可以在系统本身中很容易地证明，并且可以在提取后有效地运行。我们给出了几个实现插件的例子，包括一个参数转换。我们还提倡使用Template-Coqas作为更高级工具的基础。
Template-Coq( https://template-coq.github.io/template-coq ) is a plugin forCoq, originally implemented by Malecha [18], which provides a reifier forCoqterms and global declarations, as represented in theCoqkernel, as well as a denotation command. Initially, it was developed for the purpose of writing functions onCoq’s AST inGallina. Recently, it was used in theCertiCoqcertified compiler project [4], as its front-end language, to derive parametricity properties [3], and to extractCoqterms to a CBV-calculus [13]. However, the syntax lacked semantics, be it typing semantics or operational semantics, which should reflect, as formal specifications inCoq, the semantics ofCoq’s type theory itself. The tool was also rather bare bones, providing only rudimentary quoting and unquoting commands. We generalize it to handle the entire Calculus of Inductive Constructions (CIC), as implemented byCoq, including the kernel’s declaration structures for definitions and inductives, and implement a monad for general manipulation ofCoq’s logical environment. We demonstrate how this setup allowsCoqusers to define many kinds of general purpose plugins, whose correctness can be readily proved in the system itself, and that can be run efficiently after extraction. We give a few examples of implemented plugins, including a parametricity translation. We also advocate the use ofTemplate-Coqas a foundation for higher-level tools.