[Prev][Next][Index][Thread]
Decidability of Higher-Order Subtyping via Logical Relations
Hello,
We would like to announce the availability of our paper, Decidability
of Higher-Order Subtyping via Logical Relations, at
ftp://ftp.dcs.ed.ac.uk/pub/hhg/hosdec.ps.gz
The abstract for the paper is as follows:
This paper uses logical relations for the first time to study the
decidability of type-checking and subtyping. The result is proved
for FOmegaSub, a language with higher-order subtyping and bounded
operator abstraction not previously known to be decidable. The
proof is via an intermediate system called a typed operational
semantics, leading to a powerful and uniform technique for showing
metatheoretic results of type systems with subtyping, such as strong
normalization, subject reduction and decidability of subtyping.
Logical relations have been used for a wide variety of applications in
the syntax and semantics of type theory, for example strong
normalization following Tait and Martin-Lof, relating denotational and
operational semantics following Milne and Tait, Plotkin and others, or
operational equivalence as studied for example by Pitts. The paper
exhibits a counterexample to show that the existing methods of Pierce
and Steffen and of Chen for showing decidability of subtyping do not
extend to the system with bounded operator abstraction. Hence using
logical relations both gives a technique for showing new results, and
relates the study of subtyping to the wider body of results about type
theory.
Yours,
Adriana COMPAGNONI
Healfdene GOGUEN