Refinement types for precisely named cache locations

TL;DR

This paper introduces a refinement type system to verify that cache location names in incremental programs are used precisely, ensuring correct change propagation and enabling static reasoning about naming strategies.

Contribution

It defines and proves the soundness of a new type system that verifies precise naming in incremental computation programs, addressing an open problem.

Findings

Type system successfully verifies precise cache naming

Demonstrates applicability to programs over sequences and sets

Provides insights into dynamic naming strategies

Abstract

Many programming language techniques for incremental computation employ programmer-specified names for cached information. At runtime, each name identifies a "cache location" for a dynamic data value or a sub-computation; in sum, these cache location choices guide change propagation and incremental (re)execution. We call a cache location name precise when it identifies at most one value or subcomputation; we call all other names imprecise, or ambiguous. At a minimum, cache location names must be precise to ensure that change propagation works correctly; yet, reasoning statically about names in incremental programs remains an open problem. As a first step, this paper defines and solves the precise name problem, where we verify that incremental programs with explicit names use them precisely. To do so, we give a refinement type and effect system, and prove it sound (every well-typed program uses names precisely). We also demonstrate that this type system is expressive by verifying example programs that compute over efficient representations of incremental sequences and sets. Beyond verifying these programs, our type system also describes their dynamic naming strategies, e.g., for library documentation purposes.