coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Formalization of Liskov-Myers/Jif/... ?

From: Randy Pollack <rpollack AT inf.ed.ac.uk>
To: isabelle-users AT cl.cam.ac.uk, coq-club AT inria.fr, stevez AT cis.upenn.edu
Subject: [Coq-Club] Formalization of Liskov-Myers/Jif/... ?
Date: Thu, 24 Feb 2011 11:44:25 -0500
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=jtCV7bmFw0BJOC8vryICDDc2OKG+/YJIO6cclnt/TcGO852rHN4caqQVHzaNbkqodU YAoYv4CnE7fahJHL+Nbb6l1Km0ymlKea8oBtOj6rvC3aOSIB7DOs0srUyYYR/e18PULO Wz18mquaHf3S+k7RX+3ll1CDcyI10ETSqigEw=

Please point me to any formalization of the Liskov-Myers/Jif approach,
or descendents of it.

I have found the Isabelle AFS work on VolpanoSmith and InformationFlowSlicing.

Thanks for any info.

Randy

[Coq-Club] Formalization of Liskov-Myers/Jif/... ?, Randy Pollack