The Coq mailing list

[Marino Miculan <miculan AT dimi.uniud.it>]

Hello,

On 10/feb/07, at 12:01, 
coq-club-request AT pauillac.inria.fr
 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.
>
> -mulhern

You may consider the following work

Alberto Ciaffaglione, Marino Miculan and Luigi Liquori
Reasoning about Object-based Calculi in (Co)Inductive Type Theory and  
the Theory of Contexts.
To appear on J. Automated Reasoning, 2007.
http://www.dimi.uniud.it/miculan/Papers/JAR06.pdf

where a formal proof in Coq of type-soundness for a version of the  
sigma-calculus with references is given.

cheers
-m

--
Marino Miculan - http://www.dimi.uniud.it/miculan/
Department of Mathematics and Computer Science, University of Udine
via delle Scienze 206, 33100 Udine - Italy  --  skype: marinomiculan
vox: +39-043255-8486 - fax: +39-043255-8499 - mob: +39-3292606452