  This reports introduces a novel sound and complete semantics for first order
intuitionistic logic, in the framework of category theory and by the
computational interpretation of the logic based on the so-called Curry-Howard
isomorphism. Aside, a sound and complete semantics for the corresponding
lambda-calculus is derived, too. This semantics extends, in a way, the more
traditional meanings given by Heyting categories, the topos-theoretic
interpretation, and Kripke models. The feature which justifies the introduction
of this novel semantics is the fact that it is 'point-free', i.e., there is no
universe whose elements are used to interpret the logical terms. In other
words, terms do not denote individuals of some collection but, instead, they
denote the 'glue' which keeps together the interpretations of statements,
similarly to what happens in formal topology. Since the proposed semantics can
be trivially extended to all the first-order logical theories based on the
intuitionistic system (and, with some care, to minimal systems as well), the
semantics covers also all the predicative theories, even if some peculiar
aspects of these theories should be remarked.
