Abstract

When introducing subtypes into pure type systems (PTS), the unified syntax makes the metatheory complicated. Subtyping relations now need to consider terms, which causes mutual dependency of subtyping and typing relations. We propose a technique to solve this problem by simultaneously tracking types when defining subtyping relations. Typing becomes just syntactic sugar of subtyping, which eliminates the mutual dependency. We study the metatheory of two systems with this technique applied to show its feasibility.