DIPARTIMENTO DI
INFORMATICA Università di Torino | |
Research on "Formal Methods in Computing" Subtyping in logical formUgo de' LiguoroABSTRACT. 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.
BIBTEX. @inproceedings{deLiguoro:ITRS-02, author = {Ugo {de' Liguoro}}, title = {{Subtyping in logical form}}, booktitle = {{ITRS'02}}, year = {2002}, publisher = {Elsevier}, series = {ENTCS 70} } |
Last update: Nov 08, 2002 | |