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.

Appeared as:

@Article {Bakel-JLC'93,

Author = "S. van Bakel",
Title = "Principal type schemes for the {S}trict {T}ype {A}ssignment {S}ystem",
Journal = "Logic and Computation",
Volume = "3",
Number = "6",
Year = "1993",
Pages = "643-670"
}