Type assignment for intersections and unions in call-by-value languages

Abstract. We develop a system of type assignment with intersection types, union types, indexed types, and universal and existential depen-dent types that is sound in a call-by-value functional language. The com-bination of logical and computational principles underlying our formu-lation naturally leads to the central idea of type-checking subterms in evaluation order. We thereby provide a uniform generalization and ex-planation of several earlier isolated systems. The proof of progress and type preservation, usually formulated for closed terms only, relies on a notion of definite substitution.