Subtyping in Logical Form |
| |
Authors: | Ugo de'Liguoro |
| |
Affiliation: | aDipartimento di Informatica, Università di Torino, c.so Svizzera 185, 10149 Torino, Italy |
| |
Abstract: | 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. |
| |
Keywords: | |
本文献已被 ScienceDirect 等数据库收录! |
|