论文标题
改进类型：教程
Refinement Types: A Tutorial
论文作者
论文摘要
细化类型以逻辑谓词的形式丰富了语言的类型系统，这些系统限制了该类型所描述的值集，从而为软件开发人员提供了可调旋钮，可以通过该旋钮将其告知类型系统的不变性和正确性属性应检查其代码。在本文中，我们将有关改进类型的大量文献中提出的思想提炼成一个统一的教程，该教程解释了现代改进类型系统的关键要素。特别是，我们通过语言的进程来展示如何实现细化类型的检查器，这些语言会逐步将功能添加到语言或类型系统中。
Refinement types enrich a language's type system with logical predicates that circumscribe the set of values described by the type, thereby providing software developers a tunable knob with which to inform the type system about what invariants and correctness properties should be checked on their code. In this article, we distill the ideas developed in the substantial literature on refinement types into a unified tutorial that explains the key ingredients of modern refinement type systems. In particular, we show how to implement a refinement type checker via a progression of languages that incrementally add features to the language or type system.
