Inductive types and type constraints in the second-order lambda calculus (Q2639842)

From MaRDI portal
scientific article
Language Label Description Also known as
English
Inductive types and type constraints in the second-order lambda calculus
scientific article

    Statements

    Inductive types and type constraints in the second-order lambda calculus (English)
    0 references
    0 references
    1991
    0 references
    The author extends second order lambda calculus with two additional type constructors and shows strong normalization for this extended system using a method of Girard. Using this structure, he then derives a syntactical condition under which a given set of equations involving type variables and constants hold precisely when the resulting terms are normalizable.
    0 references
    0 references
    type constraints
    0 references
    second order lambda calculus
    0 references
    additional type constructors
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references