Meta-theory often accumulates by extension: we prove lemmas for simple systems, then hope they survive in richer ones. They often can, but only if we are careful about what we mean to enforce (the semantic specification) and how we implement it (the syntactic device). In simple systems these coincide; with extensions, they come apart.

This talk works through a case study from subtyping meta-theory — absence checking of type variables — to show how this gap can be bridged by sticking to the semantic specification faithfully and designing new syntactic devices to match it.

Building on the case, I’ll discuss a broader methodological problem — to what extent this discipline can be applied to other systems — and try to address it by identifying candidate instances that may be relevant.