A Type Soundness Proof for Variables in LCF ML

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Nov 01, 1995
Accession Number
ADA495068

Entities

People

  • Dennis Volpano
  • Geoffrey B. Smith

Organizations

  • Naval Postgraduate School

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Computer Programming
  • Computer Science
  • Computers
  • Information Operations
  • Information Processing
  • Judgment
  • Language
  • Programming Languages
  • Schools
  • Semantics
  • Test And Evaluation
  • Words (Language)

Fields of Study

  • Mathematics

Readers

  • Computational Linguistics
  • Mathematical Modeling and Probability Theory.