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

[Karl Crary]

For a formal proof of type soundness for references in Twelf, you can 
look at our recent POPL paper on mechanizing the metatheory of Standard 
ML in Twelf.  The language we formalize supports references and some 
other imperative features as well.  The proof is publicly available at 
http://www.cs.cmu.edu/~crary/papers/.

    -- Karl Crary


mulhern wrote:
> From: mulhern <mulhern at gmail.com>
> Date: February 9, 2007 10:16:37 PM EST
> To: types-list at lists.seas.upenn.edu, coq-club at pauillac.inria.fr
> Subject: [TYPES] Formal proof of type-soundness for references in Coq
>
> [ The Types Forum, 
> http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> 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