A Simplified Account of Polymorphic References. Revised
Abstract
The extension of Damas and Milner's polymorphic type system for pure functional programs (2) to accommodate mutable cells has proved to be problematic. The naive extension of the pure language with operations to allocate a cell, and to retrieve and modify its contents is unsound. The problem has received considerable attention, notably by Damas. Tofte, and Leroy and Weiss. Tofte's solution is based on a greatest fixed point construction to define the semantic typing relation. This method has been subsequently used by Leroy and Weiss and Talpin and Jouvelor. It was subsequently noted by Wright and Felleisen that the proof of soundness can be substantially simplified if the argument is made by induction on the length of an execution sequence, rather than on the structure of the typing derivation. Using this method they establish the soundness of a restriction of the language to require that let-bound expressions be values. In this note we present an alternative proof of the soundness of Tofte's imperative type discipline using a semantic framework that is intermediate between that of Wright and Felleisen and that of Tofte. The formalism considered admits a very simple and intuitively appealing proof of the soundness of Tofte's type discipline, and may be of some use in subsequent studies of this and related problems.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jun 01, 1993
- Accession Number
- ADA269182
Entities
People
- Robert Harper
Organizations
- Carnegie Mellon University