AI 中文总结
研究现代需求下类型安全验证问题，提出基于路径敏感类型化案例规范、分离类型、严格区分运行时与编译时错误及数据结构不变性类型谓词构建框架，能统一多种类型，含GADTs和液态类型，通过轻量级过程验证，还产生自验证类型检查器。
AI 中文摘要
传统上，类型安全依赖精心设计的类型系统，秉持‘类型良好的程序不会出错’的理念。现代需求推动类型系统超越这一基本保证，朝着内存安全（如Rust）、更强的数据结构不变性（如GADTs）和更广泛的可类型化性（如MLstruct）发展。但这一理念通过扩大被视为‘错误’的状态集来吸收这些属性，将它们归结为一个二元判定。更糟的是，每个需求通常都带来自身的扩展，难以说明各自的保证以及它们如何组合。Floyd-Hoare逻辑提供了统一基础。我们提出一个类型安全验证框架，由四个要素构建：用于路径敏感类型化的案例规范；受分离逻辑启发的分离类型，用于流敏感类型变异和必别名；Err（我们的类型跟踪的运行时错误值）和Abrt（编译时错误）之间的严格区分，得出改进后的理念‘类型良好的程序绝不应中止’；以及用于数据结构不变性的类型谓词。由于这四个要素在一个布尔代数中都是普通类型而非单独的扩展，该框架在一个类型逻辑中包含了GADTs和液态类型，涵盖从容忍Err的弱规范到消除它的强规范。子类型归结为一个可判定的空测试，因此一个轻量级过程就能服务整个框架，其可信基础中无需SMT预言机。我们在机器检查的Lean机械化中形式化了霍尔规则并证明了其正确性；通过证明反射，它产生了一个自验证类型检查器，并在一个基准套件上进行了评估。
英文摘要
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.
