Chronological Overview 
 Type-Hierarchical Overview 
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 »
InProc. of ITRS'02
SeriesENTCS 70
Year2002
PublisherElsevier
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: dL02.pdf

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},
}


 Chronological Overview 
 Type-Hierarchical Overview 
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)

Valid HTML 4.01!