Principal Type Schemes for the Strict Type Assignment System

1 December 1993

journal article
Published by Oxford University Press (OUP) in Journal of Logic and Computation

Vol. 3 (6) , 643-670
https://doi.org/10.1093/logcom/3.6.643

Abstract

We study the strict type assignment system, a restriction of the intersection type discipline, and prove that it has the principal type property. We define, for a term M, the principal pair (of basis and type). We specify three operations on pairs, and prove that all pairs deducible for M can be obtained from the principal one by these operations, and that these map deducible pairs to deducible pairs.

Keywords

STRICT TYPE
TYPE ASSIGNMENT
ASSIGNMENT SYSTEM
PRINCIPAL TYPE SCHEMES

This publication has 0 references indexed in Scilit: