The Coq mailing list

[David Pichardie <david.pichardie AT inria.fr>]

Dear Vijay,

Prolog definition can generally be translated into inductive predicate in Coq.

If you show me a (small) example, I can show you the corresponding Coq 
definition.

I presume you have a huge Prolog program, but writing a compiler may not be 
that difficult.

Your project on X10 looks exciting, let me know if me expertise can help.

David



Le 18 juil. 2014 à 13:46, Vijay Saraswat 
<vijay AT saraswat.org>
 a écrit :

> Pardon this newbie question .. would much appreciate pointers!
> 
> I have an SOS style semantics for a concurrent language (X10), written up 
> in (pure) Prolog.
> 
> Now need to prove various properties of the semantics, quantifying over all 
> programs. The properties relate (as usual) structural properties of the 
> code (e.g. the happens before relation on statements in the program) to the 
> operational properties (e.g. the sequence of labels in a transition 
> sequence of the program).
> 
> Obviously, a virtue of writing the semantics in Prolog is that one can 
> exhaustively enumerate all possible transition sequences for (small) X10 
> programs, and show whether the desired relationship holds or not.
> 
> But what we really want is to prove these properties for all X10 programs 
> :-).
> 
> Are there existing libraries in Coq which can help reason about pure Prolog 
> programs? Or will I need to rewrite the semantics in Coq...?
> 
> Best,
> Vijay
>