Research on "Formal Methods in Computing"

Subtyping object and recursive types logically

ABSTRACT. Subtyping in first order object calculi is studied with respect to the logical semantics obtained by identifying terms that satisfy the same set of predicates, as formalized through an assignment system. It is shown that equality in the full first order Sigma-calculus is modelled by this notion, which on turn is included in a Morris style contextual equivalence.

• A draft version, including some of the proofs, is available: [ps] , [pdf] . ( © Springer-Verlag )
• Slides.

BIBTEX.

@conference{vanBakeldeLiguoro:ICTCS-05,
   author    = {Staffen van Bakel, Ugo {de' Liguoro}},
   title     = {{Subtyping object and recursive types logically}},
   booktitle = {{Proceedings of ICTCS'05}},
   year      = {2005},
   publisher = {Springer},
   pages     = {66-80},
   series    = {LNCS 3701}
}