U. de' Liguoro
Subtyping in logical form
In Proceedings of ITRS'02, volume 70.1 of ENTCS, page 16,
2002
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.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43