The Coq mailing list

[G�rard Huet <Gerard.Huet AT inria.fr>]

Hello
You may try to have a look at my ancient CMU course notes (ref 32 on  
http://pauillac.inria.fr/~huet/bib.html).
In Chapter 3 I develop logic programming, with various versions of  
definite clauses deductions, all expressed in
pure ML. This ought to give the skeleton of a Coq development. You'll  
probably need co-inductives.
Cheers
Gérard Huet

Le 25 oct. 06 à 16:27, Sean McLaughlin a écrit :

> Hello,
>
>   I'm starting a project to formalize some aspects of a mini-Prolog  
> language, and
> was wondering if anything has been done towards formalizing logic  
> programming
> in Coq.  I'm planning to use the unification code contributed by  
> Rouyer, but
> besides that I couldn't find anything.
>
> Thanks,
>
> Sean
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club