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

Abstract: It is very difficult to decide in general whether a given program meets its specification. Program extraction is a mechanism that one can automatically extract a functional program from a constructive proof, which by its very construction is correct as we

Key words: Program extraction, Coq, Constructive proof, Curry-howard isomorphism, Calculus of inductive construction