A Type-Theoretic Account of Standard ML 1996 (Version 1).

Abstract

A type-theoretic definition of a variant of the Standard ML (Revised 1996) programming language is given. The definition consists of a syntax-directed translation of SML96 programs into a typed intermediate language. The intermediate language is an explicitly-typed lambda-calculus with product, sum, recursive, and module types. The translation performs type reconstruction, handles identifier scope resolution, enforces static well-formedness conditions, and expands high-level constructs (such as pattern matching and signature matching) into uses of the more rudimentary mechanisms of the intermediate language. This document presents work in progress and is being distributed for the purpose of obtaining feedback. As such, the translation does not completely match the definition of SML96, which is itself still undergoing change.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
May 10, 1996
Accession Number
ADA309502

Entities

People

  • Chris Stone
  • Robert Harper

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Abstracts
  • Calculus
  • Compilers
  • Computer Programming
  • Computer Science
  • Computers
  • Grammars
  • Judgment
  • Language
  • Military Research
  • Notation
  • Programming Languages
  • Semantics
  • Standards
  • Test And Evaluation
  • Translations
  • Universities

Fields of Study

  • Computer science

Readers

  • Computational Linguistics
  • Mathematical Modeling and Probability Theory.