Sciweavers

Share
FOSSACS
2003
Springer

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

8 years 11 months ago
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.
Joshua Dunfield, Frank Pfenning
Added 06 Jul 2010
Updated 06 Jul 2010
Type Conference
Year 2003
Where FOSSACS
Authors Joshua Dunfield, Frank Pfenning
Comments (0)
books