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

[mulhern]

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
> <http://www.cs.wisc.edu/%7Emulhern/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
>