Technical Report: DCC-98-6

A Semantic Characterization of Descriptive Type Systems

 Mário Florido and Luís Damas

Universidade do Porto
Rua do Campo Alegre, 823 4150 Porto, Portugal
 November 1998


Traditionally type systems are defined and then proved to be sound with respect to some well chosen semantics. We argue that the definition of the systems should come from their semantics and not the opposite. We use constrained type systems to define necessary conditions for types to be descriptions of terms. We then prove the soundness with respect to those conditions of the Curry and ML type systems.

Keywords: Type systems; Semantics of programming languages