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

[David Naumann]

On Fri, 9 Feb 2007, mulhern wrote:
> Date: Fri, 9 Feb 2007 21:16:37 -0600
> From: mulhern <mulhern at gmail.com>
> 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

There was a follow-up clarifying Mulhern's interest in proof fragments,
and one from Crary on the formalization of Standard ML in POPL07.

For the record, there's other machine-checked work on languages with 
references, e.g., Nipkow's group has done type soundness for a fragment of 
Java using Isabelle/HOL.

For a language comparable to Middleweight Java [Parkinson,Pitts], I prove 
type soundness in PVS [TPHOLS 05].  The semantics is denotational, and 
type soundness is expressed as well-definedness of the semantic function, 
which has a dependent type expressing well-formedness of states and 
absence of dangling references. (It's an ancillary result since my main 
purpose is a noninterference theorem for security typing.)

That PVS model has been extended to include Java's 'interface types' and 
first-class exceptions and handlers. The domains are streamlined to 
facilitate logical relations proofs.  Type soundness has been proved as 
before.  This development is being used to formalize the JML specification 
language [Corejml 06].

The PVS source files are available online.
http://www.cs.stevens.edu/~naumann/publications/

[TPHOLS 05]
author = {David A. Naumann},
title = {Verifying a Secure Information Flow Analyzer},
year = 2005,
booktitle = {18th International Conference on Theorem Proving in Higher Order Logics {TPHOLS}},
editor = {Joe Hurd and Tom Melham},
pages = {211--226}, publisher = {Springer}, series = LNCS, volume = 3603

[Corejml 06]
title={Preliminary Definition of Core {JML}},
author={Gary T. Leavens and David A. Naumann and Stan Rosenberg},
institition={Stevens Institute of Technology},
number={CS Report 2006-07},
URL={http://www.cs.stevens.edu/~naumann/SIT-TR-2006-07a.pdf}