A Type Discipline for Program Modules

Robert Harper; Robin Milner; Mads Tofte

doi:10.1007/BFb0014988

A Type Discipline for Program Modules

Robert Harper, Robin Milner, Mads Tofte

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract / Description of output

The ML modules system 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. The treatment of structures and signatures has interesting parallels with the type assignment rules for ML given by Damas and Milner. In particular there is a notion of principal typing.

Original language	English
Title of host publication	TAPSOFT '87 Vol. 2
Subtitle of host publication	Proceedings of the International Joint Conference on Theory and Practice of Software Development Pisa, Italy, March 23–27, 1987
Pages	308-319
Number of pages	12
ISBN (Electronic)	978-3-540-47717-4
DOIs	https://doi.org/10.1007/BFb0014988
Publication status	Published - 1987

Access to Document

10.1007/BFb0014988

http://link.springer.com/chapter/10.1007%2FBFb0014988

Cite this

@inproceedings{d645869c809944ef9e03595ce2199be0,

title = "A Type Discipline for Program Modules",

abstract = "The ML modules system 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. The treatment of structures and signatures has interesting parallels with the type assignment rules for ML given by Damas and Milner. In particular there is a notion of principal typing.",

author = "Robert Harper and Robin Milner and Mads Tofte",

year = "1987",

doi = "10.1007/BFb0014988",

language = "English",

isbn = "978-3-540-17611-4",

pages = "308--319",

booktitle = "TAPSOFT '87 Vol. 2",

}

TY - GEN

T1 - A Type Discipline for Program Modules

AU - Harper, Robert

AU - Milner, Robin

AU - Tofte, Mads

PY - 1987

Y1 - 1987

N2 - The ML modules system 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. The treatment of structures and signatures has interesting parallels with the type assignment rules for ML given by Damas and Milner. In particular there is a notion of principal typing.

AB - The ML modules system 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. The treatment of structures and signatures has interesting parallels with the type assignment rules for ML given by Damas and Milner. In particular there is a notion of principal typing.

U2 - 10.1007/BFb0014988

DO - 10.1007/BFb0014988

M3 - Conference contribution

SN - 978-3-540-17611-4

SP - 308

EP - 319

BT - TAPSOFT '87 Vol. 2

ER -

A Type Discipline for Program Modules

Abstract / Description of output

Access to Document

Fingerprint

Cite this