Extracting Purely Functional Contents from Logical Inductive Types
Extracting Purely Functional Contents from Logical Inductive Types
复制标题
从逻辑归纳类型中提取纯功能内容
DOI：
--
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
Jean
中科院分区：
文献类型：
--
作者：
David Delahaye;Catherine Dubois;Jean
我们提出了一种在归纳结构演算的背景下从逻辑归纳类型中提取纯功能内容的方法。该方法基于模式一致性分析，该分析验证计算是否可以进行。所选的输入/输出以及代码生成本身。我们证明这种提取是合理的。归纳结构的微积分。最后，我们提出了一些优化，以及 Coq 证明辅助框架中设计的实现。
We propose a method to extract purely functional contents from logical inductive types in the context of the Calculus of Inductive Constructions. This method is based on a mode consistency analysis, which verifies if a computation is possible w.r.t. the selected inputs/outputs, and the code generation itself. We prove that this extraction is sound w.r.t. the Calculus of Inductive Constructions. Finally, we present some optimizations, as well as the implementation designed in the Coq proof assistant framework.