 |
DTIC ADA269182: A Simplified Account of Polymorphic References. Rev... |
 |
by Defense Technical Information Center |
 |
Thumbnail |
|
Download |
 |
Web page |
|
|
|
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. |
|
|
|
Date Published: 2018-03-12 11:23:19 |
|
Identifier: DTIC_ADA269182 |
|
Item Size: 5401114 |
|
Language: english |
|
Media Type: texts |
|
|
|
# Topics |
|
DTIC Archive; Harper, Robert; CARNEGI... |
|
|
|
# Collections |
|
dticarchive |
|
additional_collections |
|
|
|
# Uploaded by |
|
@chris85 |
|
|
|
# Similar Items |
|
View similar items |
|
|
|
PHAROS |
|
