On sets of terms with a given intersection type

Intersection Subtyping with Constructors

Gradual Intersection Types

Natural Deduction and Normalization Proofs for the Intersection Type Discipline

Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus

Strong normalization of simple types through uniform intersection types.