Subtyping in Logical Form

By using intersection types and filter models we formulate a theory of types for a -calculus with record 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 is 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.

• Type: Journal
• Year: 2002
• Where: ENTCS
• Authors: Ugo de'Liguoro
• Keywords: ENTCS 2002, Finitary Programming Logic, Intersection Types, Type Free Realizability