从构造性证明中提取程序

摘要：

通常情况下,我们很难确定一段给定的程序是否符合它的规范,程序提取是一种从构造性证明中提取函数式程序的机制,其构造特性很好地保证了生成程序的正确性.这就为我们提供了一种开发正确性软件的方法.本文基于对Coq中程序提取机制的研究,阐述了它的理论基础、实现机制及应用.

关键词：程序提取、Coq、构造性证明、Curry-Howard 同构、归纳构造演算

所属期刊栏目：34

分类号：TP3(计算技术、计算机技术)

资助基金：欧盟资助项目typesproject29001

在线出版日期：2007-07-02（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：269-272