The Coq mailing list

[Vijay Saraswat <vijay AT saraswat.org>]

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