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):

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.

Subject Categories:

  • Numerical Mathematics
  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE