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.
Reader’s guide
Important: While the eventual results (value definiteness and type preservation
and progress) are correct, their proofs in this paper are erroneous (and the machinery of
"definite substitution" is obviated). Corrected proofs
(in a slightly extended system including guarded and asserting types) appear in Chapter 2 of
the first author's dissertation.
Some of this paper's content appeared in greater detail in
an early tech report.
