• People
• Events
• Research

A Type Discipline for Program Modules

Abstract: The ML modules system [Mac86a] is organized around the notions of structure, signature, and functor. A structure is an encapsulated declaration of data types and values, a signature is a ``type'' or specification of a structure, and a functor is a function taking structures to structures. We present a static semantics for a fragment of this system in the style of Plotkin's operational semantics [Plo81]. The treatment of structures and signatures has interesting parallels with the type assignment rules for ML given by Damas and Milner [DM82]. There is a notion of principal typing.

LFCS report ECS-LFCS-87-28