coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club]Re: 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]Re: Formal proof of type-soundness for references in Coq
Date: Mon, 19 Feb 2007 20:49:06 -0600
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:to:subject:in-reply-to:mime-version:content-type:references; b=W7t8bHMwGO3fCANJPtYmOFY+WWDOpww8aimecvgYnjRIUPphLoynKHuCgStqzLOOWjElI+HwvfJdCIDNFG+v/ZjcV9T3dVjTqPZheWbJZv+B4CCRLlfts7pIHNuivWoy+I+rNv2dtCZu4J7kZ2ENwO/7A6kF/JM7OOYectOV/IA=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi!

I'ld like to clarify my last statement. Since I'm interested in proof fragments, when I say "proof of type-soundness for references", I mean a proof of type-soundness for a fragmentary language of which every syntactic element, practically, affects the store. I did not mean to include in this category formal proofs of type-soundness for larger languages which may include references.

-mulhern

On 2/9/07, mulhern <mulhern AT gmail.com> wrote:

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