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