Synthesizing Proofs from Programs in the Calculus of Inductive Constructions

We want to prove \automatically" that a program is correct with respect to a set of given properties that is a speci cation. Proofs of speci cations contain logical parts and computational parts. Programs can be seen as computational parts of proofs. They can then be extracted from proofs and be certi ed to be correct. We focus on the inverse problem : is it possible to reconstruct proof obligations from a program and its speci cation ? The framework is the type theory where a proof can be represented as a typed -term Con86, NPS90] and particularly the Calculus of Inductive Constructions Coq85]. A notion of coherence is introduced between a speci cation and a program containing annotations as in the Hoare sense. This notion is based on the de nition of an extraction function called the weak extraction. Such an annotated program can give a method to reconstruct a set of proof obligations needed to have a proof of the initial speci cation. This can be seen either as a method of prov...

• Type: Conference
• Year: 1995
• Where: MPC
• Authors: Catherine Parent
• Keywords: Computational Parts, Mathematics, MPC 1995, Proof Obligations, Speci Cation