论文库

原文摘要

Most type systems are designed to verify safety properties: the judgement $e : τ$ holds if $e$ may evaluate to any value contained in the denotation of $τ$, but nothing more. More recent type systems have considered the complementary class of reachability properties: in these systems, the typing judgment holds if $e$ must be able to evaluate to every value denoted by $τ$, and possibly more. This paper introduces a refinement type system for higher-order functional programs where types can capture both safety and reachability properties. Simultaneously supporting both is challenging because each imposes different constraints on how variable bindings in a typing context are interpreted. We address this challenge by treating typing contexts as a kind of resource that mediates which capabilities are available when typing a program. We formalize this notion by developing a resource algebra of contextual capabilities and a bunched modal context logic over this algebra. We then interpret our type system in this logic, establishing soundness with respect to a denotational semantics that unifies safety and reachability guarantees within a single typing judgement.