2026-09-22T21:02:41Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:26102 2026-09-05T19:37:00Z ddc:004 open_access

Ownership Refinement Types for Pointer Arithmetic and Nested Arrays Fujiwara, Yusuke Matsushita, Yusuke Suenaga, Kohei Igarashi, Atsushi aliasing fractional ownership program verification refinement types type systems 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 generalizing the notion of ownership to be able to refer to the indices of the outer arrays and prove the soundness of the extended type system. 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Yusuke Fujiwara and Yusuke Matsushita and Kohei Suenaga and Atsushi Igarashi 2026 Is Part Of LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ECOOP.2026.6 urn:nbn:de:0030-drops-261029 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.6 eng https://creativecommons.org/licenses/by/4.0/legalcode