Hutchins' Pure Subtype Systems (PSS) offer a unified framework for types and terms, promising significant advancements in language design for features like dependent types and higher-order subtyping. However, the theory has been hampered by a critical gap: a proof of type safety has remained an open problem for over a decade. The original attempt to prove this property relied on the conjectured commutativity of two fundamental reduction relations, equivalence and subtyping. Proving transitivity elimination, however, requires this commutativity, a property that is notoriously difficult to establish for higher-order subtyping systems. In this paper, we address this issue by introducing Machine-Based PSS (MPSS), a novel reformulation of the original system. MPSS integrates a continuation stack mechanism, reminiscent of the Krivine Abstract Machine, to keep track of arguments that are passed during function application, enabling more fine-grained reductions. This architectural change exposes crucial intermediate reduction steps that were absent in the original PSS. The primary contribution of our work is a direct proof that the equivalence and subtyping reductions in MPSS commute. This result formally establishes transitivity elimination, which is the cornerstone of the inversion lemma required for type safety. We conclude by outlining a pathway from our foundational result to a complete, type-safe system, thereby paving the way for the practical realization of PSS-based languages.

In this system description, we present an interactive type-checker for Hutchins’ Pure Subtype Systems (PSS). By blurring the distinction between types and terms, PSS features dependent types and general recursion, but the resulting theory is highly impredicative and not strongly normalising, which poses a number of known challenges for practical implementations of type-checking. We propose an interactive type-checker where the programmer drives the type-checking process by performing different actions on the program term. Our interactive type-checker is based on Emacs and is written in Emacs Lisp. We provide a motivating example involving the type-checking of a safe division function, and we show how our type-checker certifies this function is safe by implementing a rudimentary abstract interpretation on top of PSS type-checking.