coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club]Formal proof of type-soundness for references in Coq

From: mulhern <mulhern AT gmail.com>
To: types-list AT lists.seas.upenn.edu, coq-club AT pauillac.inria.fr
Subject: [Coq-Club]Formal proof of type-soundness for references in Coq
Date: Fri, 9 Feb 2007 21:16:37 -0600
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:to:subject:mime-version:content-type; b=TdMYUE9mtp1ljQyk+46oMi80xQ396Tb2hJfGxhhzvhX3rZ95QiEGA2ISqT49N58fNg3aI8TBWoo963R8CC0V1SF0X1/4wZnMWUoN2TgHthycG8NqdJlBrfkdNuQb6aRChF27TBC+0WPy8J5wPDQG9PfOxMHVVRzlXF9xfQNRmCc=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi!

I've posted a formal proof in Coq of type-soundness for references at http://www.cs.wisc.edu/~mulhern/proofs/type-soundness/references.html .

I think it might be interesting to people on the Coq list because it uses the module system.

As far as I know, there is no other publicly available formal proof of type-soundness for references available, so it might be interesting to people on the types list as well.

-mulhern

[Coq-Club]Formal proof of type-soundness for references in Coq, mulhern
- [Coq-Club]Re: Formal proof of type-soundness for references in Coq, mulhern
- <Possible follow-ups>
- Re: [Coq-Club]Formal proof of type-soundness for references in Coq, Marino Miculan