|
Abstract : |
This paper uses logical relations for the first time to study the decidability of typechecking and subtyping. The result is proved for F, 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. 1, |
