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.

翻译：我们提出了一种逻辑上有原则的基础，用于系统化地生成SMT约束，这种方式适用于任何计算效应和求值顺序，并在函数式编程语言的精化类型系统中得到应用。通过仔细融合“按值调用推送”（call-by-push-value）的焦点化变体、双向类型化以及我们新颖的值决定索引技术，我们的系统能够生成可解的SMT约束，而不需要存在性（统一）变量。我们设计了一种极化子类型关系，从而证明我们的逻辑聚焦类型化算法是健全、完备且可判定的。我们证明了我们的声明式系统相对于基本域理论指称语义的类型健全性。类型健全性相对简单地蕴含了系统的完全正确性和逻辑一致性。我们能够相对容易地获得算法和语义结果，最终源于证明理论中的焦点化技术。