一句话：用聚焦证明论方法为精化类型系统建立可判定、可靠且完备的 SMT 约束生成基础。
精化类型系统常依赖 SMT 约束生成，但缺乏逻辑上原则化的统一基础，且难以适配任意计算效应与求值顺序。本文提出一种逻辑原则化的基础：将 call-by-push-value 的聚焦变体、双向类型检查与新的“值决定索引”技术结合，构造出不含存在（合一）变量的可解 SMT 约束生成算法；同时设计极化子类型关系，证明该聚焦类型算法可靠、完备且可判定。作者用基本域论指称语义证明声明式系统的类型可靠性，并由此相对简单地推出系统的总体正确性与逻辑一致性。算法与语义结果之所以能较容易获得，根源在于聚焦这一证明论技术。
We present a logically principled foundation for systematizing, in a way that works with any computational effect and evaluation order, SMT constraint generation seen in refinement type systems for functional programming languages. By carefully combining a focalized variant of call-by-push-value, bidirectional typing, and our novel technique of value-determined indexes, our system generates solvable SMT constraints without existential (unification) variables. We design a polarized subtyping relation allowing us to prove our logically focused typing algorithm is sound, complete, and decidable. We prove type soundness of our declarative system with respect to an elementary domain-theoretic denotational semantics. Type soundness implies, relatively simply, the total correctness and logical consistency of our system. The relative ease with which we obtain both algorithmic and semantic results ultimately stems from the proof-theoretic technique of focalization.
@article{paperbot2121,
title = {Focusing on Refinement Typing},
author = {Dimitrios J. Economou and Neel Krishnaswami and Jana Dunfield},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {45},
number = {4},
year = {2023},
doi = {10.1145/3610408}
}