Completeness of intersection and union type assignment systems for call-by-value λ-models

AbstractWe study a version of intersection and union-type assignment system, union elimination rule of which is allowed only when subject of its major premiss is a value of call-by-value λ-calculus. The system is shown to be sound and complete under some abstract notion of membership relation defined over simple semantics for call-by-value λ-models, and to be invariant under call-by-value β-conversion of subjects. We prove it by constructing a filter call-by-value λ-model