Sciweavers

Share
ENTCS
2002

Subtyping in Logical Form

9 years 1 months ago
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.
Ugo de'Liguoro
Added 18 Dec 2010
Updated 18 Dec 2010
Type Journal
Year 2002
Where ENTCS
Authors Ugo de'Liguoro
Comments (0)
books