Accession Number : ADA333520

Title :   An Interpretation of Standard ML in Type Theory

Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE

Personal Author(s) : Harper, Robert ; Stone, Christopher

PDF Url : ADA333520

Report Date : 27 JUN 1997

Pagination or Media Count : 77

Abstract : We define an interpretation of Standard ML into type theory. The interpretation takes the form of a set of elaboration rules reminiscent of the static semantics given in The Definition of Standard ML. In particular, the elaboration rules are given in a relational style, exploiting indeterminacy to avoid over commitment to specific implementation techniques. Elaboration consists of identifier scope resolution, type checking and type inference, expansion of derived forms pattern compilation, overloading resolution, equality compilation, and the coercive aspects of signature matching. The underlying type theory is an explicitly typed lambda calculus with product sum function and recursive types together with module types derived from the translucent sum formalism of Harper and Lillibridge. Programs of the type theory are given a type passing dynamic semantics compatible with constructs such as polymorphic equality that rely on type analysis at run time.

Descriptors :   *COMPUTER PROGRAMMING, *PROGRAMMING LANGUAGES, *COMPILERS, SOFTWARE ENGINEERING, SEMANTICS, MACHINE CODING, CALCULUS OF VARIATIONS, POLYMORPHISM.

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE