论文标题
专注于细化打字
Focusing on Refinement Typing
论文作者
论文摘要
我们为系统化的逻辑原则化基础，以一种适用于任何计算效果和评估顺序的方式，在功能编程语言的改进类型系统中看到的SMT约束生成。通过仔细结合逐个呼叫值，双向键入的焦点变体以及我们的新颖值确定索引的新技术，我们的系统生成了可解决的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.
