[TYPES/announce] Paper on Higher-Order Subtyping

[Andreas Abel]

I'd like to announce a new paper:

   Polarized Subtyping for Sized Types (Extended Version)
   Submitted.
   http://www.tcs.ifi.lmu.de/~abel/mscs06.pdf

In this article, I consider declarative and algorithmic higher-order 
subtyping.  Completeness of algorithmic subtyping is shown via a new 
technique:  Instead of constructing a model, closure of algorithmic 
subtyping under application is proven directly using a lexicographic 
induction on kinds and derivations.  Transitivity is also shown using an 
induction on derivation.  The resulting completeness proof is concise 
and technically light-weight, and suitable for a formalization in a weak 
logical framework, for instance, the Edinburgh LF.

Best regards,
Andreas Abel

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/