Decidability of Higher-Order Subtyping via Logical Relations


We would like to announce the availability of our paper, Decidability
of Higher-Order Subtyping via Logical Relations, at

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


Healfdene GOGUEN