coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Nathan Whitehead <nwhitehe AT gmail.com>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club]Prolog in Coq
Date: Wed, 11 Jan 2006 14:35:58 -0800
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:reply-to:to:subject:mime-version:content-type; b=KThfacCY+2OC997QMnIsXe5IWxGEqGtYxQSYOFLv1CiLiPe7RRS70V+qcQyqzUVxWNPaeS5Pu1yfuk81CvSh8NWPj909dYozweb2lZjVQ/ApUemdEvBv22LSZOjQTig76JHGsuWN8V1uPUosGjsT4m7k76PVE6sQPkupkXTtHVk=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Has anyone done Prolog in Coq, and extracted a correct Prolog interpreter? (Or any kind of simplified Prolog).
--
Nathan Whitehead