technical report

• To: types@dcs.gla.ac.uk
• Subject: technical report
• From: Robert Harper <rwh@cs.cmu.edu>
• Date: Thu, 16 May 1996 16:23:35 -0400
• Approved: types@dcs.gla.ac.uk

[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

The following technical report is available from the Fox Project web page
http://foxnet.cs.cmu.edu.

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

AUTHORS: Chris Stone and Robert Harper

NUMBER: CMU-CS-96-136, CMU-CS-FOX-96-02

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.

Bob Harper
Chris Stone

• Prev: The 1996 Summer School on Advanced Functional Programming
• Next: Participation Call: TPHOLs'96 - Theorem Proving in Higher Order Logics
• Index(es):
  • Main
  • Thread