arXiv:2611.13471 · v1

Context Types: Bunched Modalities for Unifying Safety and Reachability

首次提交 2026-11-10 10:31

版本更新 2026-11-10 10:31

雷达观测 2026-11-11 11:04

摘要

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.