|
Formal Methods in Computing (Most of the papers antecedent to 1995 are not included in the list) |
|||
| FRAMES NO FRAME | ||||
| deLiguoro:ITRS-02 (In proceedings) | |
| Author(s) | Ugo de' Liguoro |
| Title | « Subtyping in logical form » |
| In | Proc. of ITRS'02 |
| Series | ENTCS 70 |
| Year | 2002 |
| Publisher | Elsevier |
| Abstract | |
| 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. | |
Download the complete article:
| BibTeX code |
@inproceedings{deLiguoro:ITRS-02,
author = {Ugo de' Liguoro},
series = {ENTCS 70},
booktitle = {{Proc. of ITRS'02}},
localfile = {http://www.di.unito.it/~deligu/pub/dL02.pdf},
title = {{Subtyping in logical form}},
abstract = {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.},
tag = {{ITRS'02}},
publisher = {Elsevier},
year = {2002},
}
|
Formal Methods in Computing (Most of the papers antecedent to 1995 are not included in the list) |
|||
| FRAMES NO FRAME | ||||
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)
