Ownership Refinement Types for Pointer Arithmetic and Nested Arrays

Abstract

Tanaka et al. proposed a type system for verifying functional correctness properties of programs that use arrays and pointer arithmetic. Their system extends ConSORT--a type system combining fractional ownership and refinement types for imperative program verification--with support for pointer arithmetic. Their idea was to extend fractional ownership so that it can depend on an array index. Their formulation, however, does not handle nested arrays, which are essential for representing practical data structures such as matrices. We extend Tanaka et al.'s type system to support nested arrays by allowing ownership to depend on the indices of enclosing arrays. We formalize the extended calculus in Rocq using a mixed embedding and provide a machine-checked proof of type soundness. We have implemented a verifier based on the proposed type system and demonstrated that it can verify the correctness of programs that manipulate nested arrays, which were beyond the reach of Tanaka et al.

arXiv commentExpanded version of our ECOOP 2026 paper, submitted for journal publication. Adds a Rocq formalization and machine-checked type soundness proof, revises the formal system and proofs, and expands the implementation and related-work discussions