A Type Soundness Proof for Variables in LCF ML

Thumbnail Image
Files
Volpano_Smith_Type_Soundness_1995.pdf (206.43 KB)
Authors
Volpano, Dennis
Smith, Geoffrey
Subjects
Advisors
Date of Issue
1995-07
Date
July 1995.
Publisher
Language
Abstract
We prove the soundness of a polymorphic type system for a language with variables assignments and rst class functions As a corollary this proves the soundness of the Edinburgh LCF ML rules for typing variables and assignments thereby settling a long standing open problem.
Type
Description
The article of record as published may be found at http://dx.doi.org/
URI
https://hdl.handle.net/10945/35279
Series/Report No
Department
Computer Science (CS)
Organization
Identifiers
NPS Report Number
Sponsors
Funder
Format
Citation
Information Processing Letters 56(3), pp. 141-146, Nov 1995. Also presented at the Newton Institute on Themes in the Semantics of Computation, Cambridge UK, July 1995.
Distribution Statement
Rights
This publication is a work of the U.S. Government as defined in Title 17, United States Code, Section 101. Copyright protection is not available for this work in the United States.
Collections
Publications