A Type Soundness Proof for Variables in LCF ML

reportActive / Technical Report | Accession Number: ADA495068 | Open PDF

Abstract:

We prove the soundness of a polymorphic type system for a language with variables, assignments, and first-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.

Author(s):
Volpano, Dennis ; Smith, Geoffrey
Author Organization(s):
NAVAL POSTGRADUATE SCHOOL MONTEREY CA DEPT OF COMPUTER SCIENCE
Descriptive Note:
Journal article
Supplementary Note:
Published in Information Processing Letters v56 n3 p141-146, Nov 1995.
Pagination:
0010

Security Markings

DOCUMENT & CONTEXTUAL SUMMARY

Distribution:
Approved For Public Release
Distribution Statement:
Approved For Public Release; Distribution Is Unlimited.

RECORD

Collection: TR
Identifying Numbers
Contract/Grant Number(s):
CCR-9400592, CCR-9414421
Monitor Series:
NSF
 Subject Terms
Joint Capability Areas:
JCA_1_Force Support; JCA_1.3_Human Capital Management; JCA_1.3.2_Personnel Management; JCA_8_Building Partnerships
Communities of Interest:
No COI(s) Identified
Descriptor(s):
*PROGRAMMING LANGUAGES, *THEOREMS, VARIABLES, SYNTAX, POLYMORPHISM, COMPUTATIONS, REPRINTS, SEMANTICS
Field(s)/Group(s):
Numerical Mathematics, Computer Programming and Software
Keyword(s):
LETVAR CONSTRUCT, COROLLARY
Report Date:
1995 Nov 01
Creation Date:
2009 Apr 01