Principal Type Schemes for the Strict Type Assignment System

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.