We investigate the foundations of reasoning over infinite data structures by means of set-theoretical structures arising in the sheaf-theoretic semantics of higher-order intuitionistic logic. Our approach focuses on a natural notion of tiering involving an operation of restriction of elements to levels forming a complete Heyting algebra. We relate these tiered objects to final coalgebras and initial algebras of a wide class of endofunctors of the category of sets, and study their order and convergence properties. As a sample application, we derive a general proof principle for tiered objects.

We characterize those type preorders which yield complete intersection-type assignment systems for λ-calculi, with respect to the three canonical set-theoretical semantics for intersection-types: the inference semantics, the simple semantics, and the F-semantics. These semantics arise by taking as interpretation of types subsets of applicative structures, as interpretation of the preorder relation , ≤, set-theoretic inclusion, as interpretation of the intersection constructor , ∩, set-theoretic intersection, and by taking the interpretation of the arrow constructor , → à la Scott, with respect to either any possible functionality set , or the largest one, or the least one.These results strengthen and generalize significantly all earlier results in the literature, to our knowledge, in at least three respects. First of all the inference semantics had not been considered before. Second, the characterizations are all given just in terms of simple closure conditions on the preorder relation , ≤, on the types, rather than on the typing judgments themselves. The task of checking the condition is made therefore considerably more tractable. Last, we do not restrict attention just to λ-models, but to arbitrary applicative structures which admit an interpretation function. Thus we allow also for the treatment of models of restricted λ-calculi. Nevertheless the characterizations we give can be tailored just to the case of λ-models.

To model at the same time parallel and nondeterministic functional calculi we define a powerdomain functor Ρ such that it is an endofunctor over the category of algebraic lattices. Ρ is locally continuous and we study the initial solution D ∞ of the domain equation D = Ρ([D → D] ⊥ ). We derive from the algebras of Ρ the logic of D ∞ , that is the axiomatic description of its compact elements. We then define a λ-calculus and a type assignment system using the logic of D ∞ as the related type theory. We prove that the filter model of this calculus, which is isomorphic to D ∞ , is fully abstract with respect to the observational Preorder of the λ-calculus.

A model is given for the second-order lambda calculus extended with inheritance, bounded quantification, recursive types, constructors and kinds. This language, called mu -FunK, can be viewed as the core of the QUEST language defined by L. Cardelli (SRC Rep. 45, 1989). Types are interpreted as intervals of partial equivalence relations. Because of the properties of intervals and their ordering, all the type constructors are continuous functions. As a consequence a system where a kind is given to each constructor constant employed can be modeled. In such a model the meaning of operator mu , the constructor of recursive types, turns out to be just the minimal fixed-point operator.>