Sciweavers

MPC
1995
Springer
125views Mathematics» more  MPC 1995»
14 years 3 months ago
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 ...
Catherine Parent