Tofte, Mads

2013-04-02T15:15:37Z

2013-04-02T15:15:37Z

1988

Three languages with polymorphic type disciplines are discussed, namely the λ-calculus with Milner's polymorphic type discipline; a language with imperative features (polymorphic references); and a skeletal module language with structures, signatures and functors. In each of the two first cases we show that the type inference system is consistent with an operational dynamic semantics. On the module level, polymorphic types correspond to signatures. There is a notion of principal signature. So-called signature checking is the module level equivalent of type checking. In particular, there exists an algorithm which either fails or produces a principal signature.

http://hdl.handle.net/1842/6606

en

The University of Edinburgh

R. Harper, R. Milner and M. Tofte, A type discipline for program modules, Proc. TAPSOFT '87, Springer, Lecture Notes in Computer Science 250, Berlin - Heidelberg - New York, 1987, 308-319.

R. Harper, R. Milner and M. Tofte, The semantics of Standard ML, Version 1, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, ECS-LFCS-87-36, 1987

λ-calculus

skeletal module language

polymorphic types

Operational Semantics and Polymorphic Type Inference

Thesis or Dissertation

Doctoral

PhD Doctor of Philosophy