Refinement types decorate types with assertions that enable automatic verification. Like assertions, refinements are limited to binders that are in scope, and hence, cannot express higher-order specifications. Ghost variables circumvent this limitation but are prohibitively tedious to use as the programmer must divine and explicate their values at all call-sites. We introduce Implicit Refinement Types which turn ghost variables into implicit pair and function types, in a way that lets the refinement typechecker automatically synthesize their values at compile time. Implicit Refinement Types further take advantage of refinement type information, allowing them to be used as a lightweight verification tool, rather than merely as a technique to automate programming tasks. We evaluate the utility of Implicit Refinement Types by showing how they enable the modular specification and automatic verification of various higher-order examples including stateful protocols, access control, and resource usage.

翻译：与断言一样,改进仅限于范围广、因此无法表达更高顺序规格的捆绑物。 幽灵变量绕过这一限制,但却令人无法忍受地使用,因为程序设计者必须在所有呼叫站点施展其价值。 我们引入了将幽灵变量变成隐含对和功能类型的隐性精细类型,使精细类型检查器能够在编译时自动合成其价值。 隐性精细精细类型进一步利用精细类型信息,允许它们用作轻量级核查工具,而不仅仅是将编程任务自动化的一种技术。我们评估了不完全精细类型的作用,展示了它们如何使模块规格和自动核查各种更高顺序的例子,包括状态协议、访问控制和资源使用。