Towards the type safety of Pure Subtype Systems (Full version)

Valentin Pasquale, Álvaro García-Pérez

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 high…