F-semantics for intersection type discipline

Abstract

Aim of this paper is to investigate the soundness and completeness for the F-semantics (F-soundness and F-completeness) of some modifications of the intersection type discipline for terms of the (untyped) λ-calculus. As pointed out by Scott, the key of a λ-model is the set F of the elements representing functions. The F-semantics of types takes into account that the intuitive meaning of “ δ → τ ” is “a function with domain δ and range τ ” and interprets δ → τ as a subset of F. The type theories which induce F-complete type assignments are characterized. It results that a type assignment is F-complete iff the following are derived rules for it: {ie279-1}