Search papers, labs, and topics across Lattice.
This paper introduces a unified framework for type-safety verification that integrates four key components: path-sensitive typing, separation types, a refined distinction between runtime and compile-time errors, and type predicates for data-structure invariants. By consolidating these elements into a single type logic, the framework effectively encompasses advanced type systems such as GADTs and liquid types while simplifying subtyping to a single decidable emptiness test. The approach is formalized through machine-checked proofs in Lean, resulting in a self-certifying type-checker that demonstrates soundness across a benchmark suite.
A unified type-safety framework that simplifies complex type systems into a single logic, ensuring well-typed programs never abort.
Type safety has traditionally rested on carefully crafted type systems, under the motto"well-typed programs cannot go wrong". Modern demands push type systems past this basic guarantee: toward memory safety (e.g., Rust), stronger data-structure invariants (e.g., GADTs), and broader typability (e.g., MLstruct). The motto absorbs each such property by enlarging the set of states deemed"wrong", but collapses them into one binary verdict: heap ownership, flow-sensitive changes to a variable's type, and the gap between a recoverable and a fatal error are relational, stateful facts about intermediate states that one verdict cannot tell apart. Worse, each demand typically brings its own extension, making it hard to say what each guarantees or how they combine. Floyd-Hoare logic supplies a unified foundation. We present a framework for type-safety verification built from four ingredients: (i) case specifications for path-sensitive typing; (ii) separation types, inspired by separation logic, for flow-sensitive type mutation and must-aliasing; (iii) a disciplined distinction between Err (runtime error values our types track) and Abrt (compile-time errors), yielding the refined motto well-typed programs must never abort; and (iv) type predicates for data-structure invariants. Since all four are ordinary types in one Boolean algebra rather than separate extensions, the framework subsumes both GADTs and liquid types within one type logic, spanning weak specifications that tolerate Err to strong ones that eliminate it. Subtyping reduces to one decidable emptiness test, so a single lightweight procedure serves the whole framework with no SMT oracle in its trusted base. We formalise the Hoare rules and prove soundness in a machine-checked Lean mechanisation; by proof reflection it yields a self-certifying type-checker, evaluated on a benchmark suite.
