Titolo:
Logical semantics and PER models

Autore:
Ugo De' Liguoro

By using intersection types and filter models we formulate a theory of
subtyping via a finitary programming logic. Types are interpreted as
spaces of filters over a subset of the language of properties (the
intersection types) which describes the underlying type free
realizability structure. We show that such an interpretation coincides
with a PER semantics, proving that the quotient space arising from
``logical'' PERs taken with the intrinsic ordering is isomorphic to
the filter semantics of types. As a byproduct we obtain a semantic
proof of soundness of the logic semantics of terms and equation of a
typed lambda calculus with record subtyping.