Type-soundness for references

The proof is based on the development in Chapter 13 of Pierce's "Types and Programming Languages". The language and development is exactly as in the chapter, except that the terms, types, typing schemas, etc., having to do with variables, lambda abstraction, and lambda application have been omitted. The intention of the development is that it should serve as a proof fragment and that it might be reused for constructing larger proofs of type-soundness for more complex languages of which references are a part. The development is in Coq.

Since stores and store typings are required to have similar behaviors the development defines a single Coq module, Map_Wf_Ext (an extensible, well-formed map structure) parameterized on the type of the value that is stored. Map_Wf_Ext uses natural numbers as the indices to the store.

Files included in the developement are:

• references.v Defines the rules of the fragmentary language. Builds the store and store typing from the Map_Wf_Ext module. Includes the proof of progress and preservation.
• store.v Defines the Map_Wf_Ext module. This module is built on the underlying Map module, but also includes proofs of well-formedness and can be extended with new values via the functions allocate and add.
• map.v Defines the module Map, a partial function from indices to values. The values may be of any type that implements the OPTION module type.
• util.v Declares the module types VALUE and OPTION and provides an implementation of OPTION, Option.

A tar file of the sparsely commented source code is available here.