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
Type theory
formal semantics
variables and assignment
Advisors
Date of Issue
1995-11
Date
Publisher
Elsevier
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
Article
Description
URI
https://hdl.handle.net/10945/35279
Series/Report No
Department
Computer Science (CS)
Organization
Identifiers
NPS Report Number
Sponsors
National Science Foundation
Funder
Agreement No. CCR-9400592
Agreement No. CCR-9414421
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