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

FOSSACS '03 (Warsaw, April 2003)

Jana Dunfield and Frank Pfenning

Abstract

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

warning sign 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.

Conference slides

Final version (January 2003)

BibTeX entry

  @InProceedings{Dunfield03:IntersectionsUnionsCBV,
    author =    {Jana Dunfield and Frank Pfenning},
    title =     {Type Assignment for Intersections and Unions in Call-by-Value Languages},
    booktitle = {Foundations of Software Science and Computation Structures (FOSSACS '03)},
    pages =     {250--266},
    year =      2003,
    editor =    {A.D. Gordon},
    address =   {Warsaw, Poland},
    month =     apr,
    publisher = {Springer-Verlag LNCS 2620}
  }

all papers * related papers

J. Dunfield