[TYPES] Formal proof of type-soundness for references in Coq
mulhern at gmail.com
Mon Feb 19 21:49:06 EST 2007
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
On 2/9/07, mulhern <mulhern at gmail.com> wrote:
> 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.
More information about the Types-list