Skip to Content.
Sympa Menu

coq-club - [Coq-Club]Re: [TYPES] Formal proof of type-soundness for references in Coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


chronological Thread 
  • From: Karl Crary <crary AT cs.cmu.edu>
  • To: types-list AT lists.seas.upenn.edu, coq-club AT pauillac.inria.fr, mulhern AT gmail.com
  • Subject: [Coq-Club]Re: [TYPES] Formal proof of type-soundness for references in Coq
  • Date: Mon, 12 Feb 2007 11:53:43 -0500
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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





Archive powered by MhonArc 2.6.16.

Top of Page