coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Help-Cannot find the Coq proof of polychronous protocol for LTTA.

From: prateek agarwal <prateek.iitkgp AT gmail.com>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Help-Cannot find the Coq proof of polychronous protocol for LTTA.
Date: Tue, 17 Feb 2009 16:07:29 +0530
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:date:x-google-sender-auth:message-id:subject :from:to:content-type; b=doyK674rntQKA/k6aJZ/1+EytRi01fdvt2iE1RzH4OH5JK15m8ZeBHPRrxzoq5z7UT 4WNVDDjAC12jH/zAoF4TEEu5Z3vgG5FPu3esHz+t/WBuDhYLzNUrAaN2IeVWOkG/jUSY X5ilZzCnDpyqJrWtu6kt8AVqaX1+SWERPDbeg=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi,
I have searched the net for Coq proof given in the paper "Formal Proof of a Polychronous Protocol
for Loosely Time-Triggered Architectures", but could not found any. Actually the proof in the paper is not completely given in Coq. So it would be great if I could get the proof for that protocol in Coq.

Thanks a lot.
--
Prateek Agarwal
4th yr. Undergraduate Student
Dept. of Computer Science And Engg.
Indian Institute of Technology, Kharagpur
India.

[Coq-Club] Help-Cannot find the Coq proof of polychronous protocol for LTTA., prateek agarwal