Accession Number:

ADA495068

Title:

A Type Soundness Proof for Variables in LCF ML

Descriptive Note:

Journal article

Corporate Author:

NAVAL POSTGRADUATE SCHOOL MONTEREY CA DEPT OF COMPUTER SCIENCE

Personal Author(s):

• Volpano, Dennis
• Smith, Geoffrey

Report Date:

1995-11-01

Pagination or Media Count:

10.0

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.

Descriptors:

• *PROGRAMMING LANGUAGES
• *THEOREMS
• VARIABLES
• SYNTAX
• POLYMORPHISM
• COMPUTATIONS
• REPRINTS
• SEMANTICS

Subject Categories:

• Numerical Mathematics
• Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE