The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT univ-orleans.fr>]

On Wed, 17 Mar 2004 17:49:56 +0100
"Joseph N. Ruskiewicz" 
<joseph.ruskiewicz AT inf.ethz.ch>
 wrote:

>    The approach that I will be taking will be from the B side and not 
> the C/Java side.
> 
>     So, taking a formal method and then generating the proofs into Coq 
> for proving.

Hi,

You mean you want to somehow use Coq to prove the proof obligations
generated by B (or another specif system)? I am not sure Why will be
directly helpful to you as it takes *programs* as input instead of
specifications. 

A possible approach would be a translation from B specifs to axiomatically
defined coq functions (that may ultimately be implemented (and proved
correct) at the last refinement step). Exciting!

Cheers,

Pierre