Type Assignment for Intersections and Unions in Call-by-Value Languages

We develop a system of type assignment with intersection types, union types, indexed types, and universal and existential dependent types that is sound in a call-by-value functional language. The combination of logical and computational principles underlying our formulation naturally leads to the central idea of type-checking subterms in evaluation order. We thereby provide a uniform generalization and explanation 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.

• Type: Conference
• Year: 2003
• Where: FOSSACS
• Authors: Joshua Dunfield, Frank Pfenning
• Keywords: Applied Computing, Call-by-value Functional Language, Existential Dependent Types, FOSSACS 2003, Intersection Types