pith. machine review for the scientific record. sign in

arxiv: 2604.22361 · v1 · submitted 2026-04-24 · 💻 cs.PL

Recognition: unknown

Ownership Refinement Types for Pointer Arithmetic and Nested Arrays

Yusuke Fujiwara , Yusuke Matsushita , Kohei Suenaga , Atsushi Igarashi
Authors on Pith no claims yet

Pith reviewed 2026-05-08 08:43 UTC · model grok-4.3

classification 💻 cs.PL
keywords ownership typesrefinement typesnested arrayspointer arithmeticprogram verificationtype soundnessimperative programs
0
0 comments X

The pith

Generalizing ownership to reference outer array indices lets a type system verify programs with nested arrays and pointer arithmetic.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper extends an existing type system that combines fractional ownership with refinement types so that it can handle nested arrays. The key change is to let ownership predicates refer to indices of outer arrays, which tracks permissions across multiple levels of nesting. This supports verification of functional correctness for practical structures like matrices while retaining pointer arithmetic. The authors prove the extended system remains sound, so well-typed programs satisfy their specifications. They also built a verifier that succeeds on examples the prior system could not check.

Core claim

We generalize the ownership component of the type system to allow references to the indices of outer arrays in nested structures. This extension, together with the retained support for pointer arithmetic, permits verification of functional correctness properties for programs that manipulate nested arrays. We prove that the resulting type system is sound.

What carries the argument

Generalized ownership that can depend on outer-array indices, which tracks permissions across nesting levels while preserving the original refinement and soundness properties.

If this is right

  • Programs that manipulate matrices or other nested arrays can be verified for functional correctness properties.
  • Pointer arithmetic inside nested structures remains verifiable under the same soundness guarantee.
  • The implemented verifier succeeds on examples that previous systems rejected as out of scope.
  • Well-typed programs are guaranteed to respect the ownership and refinement constraints stated in their types.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same generalization technique could be applied to other nested memory structures such as multi-dimensional tensors.
  • Automation of ownership inference might become feasible once the rules for outer indices are fixed.
  • Integration with existing refinement type checkers for C-like languages could broaden the set of verifiable low-level data layouts.

Load-bearing premise

The generalization of ownership to outer indices preserves the original system's key invariants without introducing inconsistencies in the typing rules or ownership accounting.

What would settle it

A concrete program containing nested arrays and pointer arithmetic that the type checker accepts yet violates its refinement specification or exhibits an out-of-bounds access at runtime would falsify the soundness claim.

read the original 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 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper extends Tanaka et al.'s ownership refinement type system (itself extending ConSORT with index-dependent fractional ownership for pointer arithmetic) to nested arrays. The key generalization allows ownership predicates to refer to indices of enclosing arrays (e.g., own(1/2, a[i][j]) where i is an outer-array index). The authors prove soundness of the extended system, implement a verifier, and demonstrate verification of programs manipulating nested arrays that were out of reach for the prior system.

Significance. If the soundness argument holds, the work meaningfully broadens the class of verifiable imperative programs with practical data structures such as matrices. The implementation and concrete verification examples constitute a clear strength, providing evidence of applicability beyond the theoretical extension. The independent soundness proof (rather than reduction to prior results) is also a positive feature.

major comments (2)
  1. [§5] §5 (Soundness): The central claim rests on preservation of the original ConSORT/Tanaka fractional invariants (fractions sum to ≤1, refinements stable under updates, no aliasing violations) after generalizing ownership to outer indices. The provided proof sketch must explicitly address how index-dependent fractions behave under pointer arithmetic on inner arrays; without a concrete lemma showing that nested access rules cannot duplicate tokens or produce inconsistent fractions across levels, the extension's soundness cannot be fully assessed.
  2. [§4.3] §4.3 (Typing rules for nested access): The new rules for array indexing that bind outer indices into ownership predicates must be shown not to introduce cases where an inner-array ownership token can be duplicated via arithmetic on the outer array. A worked example of the preservation case for a pointer-arithmetic step on a nested array would strengthen the argument.
minor comments (2)
  1. [§3] Notation for generalized ownership (e.g., the precise syntax of predicates that mention outer indices) should be introduced earlier and used consistently in the examples of §6.
  2. [§6] The evaluation section would benefit from a table summarizing the verified programs, their sizes, and which features (nested arrays, pointer arithmetic) each exercises.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive comments and positive evaluation of the significance of our work on extending ownership refinement types to nested arrays. We address each major comment below and will revise the manuscript to strengthen the presentation of the soundness argument.

read point-by-point responses

  1. Referee: [§5] §5 (Soundness): The central claim rests on preservation of the original ConSORT/Tanaka fractional invariants (fractions sum to ≤1, refinements stable under updates, no aliasing violations) after generalizing ownership to outer indices. The provided proof sketch must explicitly address how index-dependent fractions behave under pointer arithmetic on inner arrays; without a concrete lemma showing that nested access rules cannot duplicate tokens or produce inconsistent fractions across levels, the extension's soundness cannot be fully assessed.

    Authors: We agree that the proof sketch in §5 would be strengthened by an explicit lemma on the behavior of index-dependent fractions under pointer arithmetic involving inner arrays. The current argument generalizes the preservation of fractional invariants from Tanaka et al. by treating outer indices as parameters in ownership predicates, which ensures that fractions continue to sum to at most 1 and that no aliasing violations arise. However, to make the case analysis fully explicit, we will add a dedicated lemma in the revised §5 that covers nested pointer-arithmetic steps, showing preservation of the invariants across array levels without token duplication or inconsistent fractions. revision: yes

  2. Referee: [§4.3] §4.3 (Typing rules for nested access): The new rules for array indexing that bind outer indices into ownership predicates must be shown not to introduce cases where an inner-array ownership token can be duplicated via arithmetic on the outer array. A worked example of the preservation case for a pointer-arithmetic step on a nested array would strengthen the argument.

    Authors: We agree that a concrete worked example would improve the clarity of the typing rules in §4.3. The rules are formulated so that outer indices are bound as parameters in the ownership predicates, preventing duplication because arithmetic on the outer array updates the index values in a way that respects the existing fractional ownership. In the revision we will include a detailed preservation example for a pointer-arithmetic step on a nested array (e.g., incrementing a pointer into an inner array while an outer index is in scope), demonstrating that no additional ownership tokens are created. revision: yes

Circularity Check

0 steps flagged

No significant circularity; extension and soundness proof are independent of inputs by construction.

full rationale

The paper extends Tanaka et al. by generalizing ownership to reference outer-array indices and states that it proves soundness of the resulting system. No equations or rules reduce the claimed result to a prior fit, self-definition, or self-citation chain; the soundness argument is presented as newly established rather than inherited by renaming or construction. The derivation introduces new typing rules for nested arrays without any of the enumerated circular patterns.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The claim rests on standard properties of refinement types and ownership (e.g., fractional permissions compose correctly) plus the new generalization; no free parameters or invented entities are introduced.

axioms (1)
  • standard math Standard soundness properties of refinement type systems and fractional ownership hold for the base ConSORT system
    Invoked when extending the system and claiming the extension remains sound.

pith-pipeline@v0.9.0 · 5447 in / 1127 out tokens · 41265 ms · 2026-05-08T08:43:36.359307+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

31 extracted references · 1 canonical work pages

  1. [1]

    URL: https://link.springer.com/chapter/10.1007/978-3-662-48288-9_12, doi:10.1007/978-3-662-48288-9_12

    Springer, 2015. URL: https://link.springer.com/chapter/10.1007/978-3-662-48288-9_12, doi:10.1007/978-3-662-48288-9_12. 16 David L. Heine and Monica S. Lam. A practical flow-sensitive and context-sensitive C and C++ memory leak detector. In Ron Cytron and Rajiv Gupta, editors,Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and...

    work page doi:10.1007/978-3-662-48288-9_12 2015

  2. [2]

    Ownership terms can be specified by ref(l, h, o) , which representsΠx.(···refx∈[l,h]⇒o)

    Function annotations: Function definitions often require explicit ownership annotations for reference types and refinements for integer types. Ownership terms can be specified by ref(l, h, o) , which representsΠx.(···refx∈[l,h]⇒o). Furthermore, integer arguments must be explicitly marked with a # to indicate that they may appear in ownership terms

  3. [3]

    letx=_inebindsxto the type{ν:int|⊤}(an arbitrary integer)

    Indeterminate integer literals (_): We introduce a syntax for indeterminate integer values. letx=_inebindsxto the type{ν:int|⊤}(an arbitrary integer). In this notation, it is also possible to specify a refinement type. For example,letx = 0in lety=_: (y > x)inebindsyto a positive integer. Formally, the syntax is:e::=letx=_ine|letx=_: (φ)ine lety = _: (y > ...

  4. [4]

    When written asletx =y⊞zine , this represents array partitioning

    Pointer arithmetic: We explicitly distinguish between partitioning and sharing in pointer arithmetic. When written asletx =y⊞zine , this represents array partitioning. It transfers all ownership from thez-offset point (relative to wherex points) onward toy, and the part beforezis not transferred toyat all. When written aslet immutx =y⊞zine , this represen...

  5. [5]

    letx=∗yine: All ownership of the head element ofyis transferred tox

    Ownership distribution: We heavily restrict the methods of ownership distribution for array reads, writes, and alias expressions. letx=∗yine: All ownership of the head element ofyis transferred tox. Y. Fujiwara, Y. Matsushita, K. Suenaga and A. Igarashi 33 x: =y;e: All ownership ofyis transferred to the head element ofx. alias(x=y⊞z) ;e: All ownerships he...

  6. [6]

    ≈” counts benchmarks with ratio< 1.05×. “Rev

    Automated insertion ofalias expressions: Our verifier implements the following simple automated insertion ofalias expressions to reduce the annotation burden on programmers. In e of letx =∗yine, if there is an expression that creates a new binding throughy (i.e., an expression of the formletz =∗yine1 or letz =y⊞nine 1), thenalias(x =∗y) is automatically i...

    2011

  7. [7]

    and 2,Θ |Γ[y :{ν: int|φ}],z: Πw.({ν: int|0 ≤w∧w≤y−1 =⇒ν= 0}refr),x:τx⊢e0 : τ⇒Γ′,z:τ′,x:τx holds

    Θ |Γ[y :{ν: int|φ}],z: Πw.({ν: int|0≤w∧w≤y−1 =⇒ν= 0}refr)⊢e0 : τ⇒Γ′,z:τ′ By I.H. and 2,Θ |Γ[y :{ν: int|φ}],z: Πw.({ν: int|0 ≤w∧w≤y−1 =⇒ν= 0}refr),x:τx⊢e0 : τ⇒Γ′,z:τ′,x:τx holds. Because x is fresh, the update fromΓto Γ,x:τx does not affect ownership term, that is, Γ,w:int|=r= ((0≤w∧w≤y−1)⇒1,0)⇐⇒Γ,x:τx,w:int|=r= ((0≤w∧w≤y−1)⇒1,0). From the rule T-MkIntArra...

  8. [8]

    Finally, S-RefshowsΓ⊢τ1≤τ3

    Also,Γ ,z:int|=r1 ≥r3 holds. Finally, S-RefshowsΓ⊢τ1≤τ3. the proof of reflexivity ofΓ≤Γ′ It easily follows from the reflexivity ofΓ⊢τ1≤τ2. the proof of transitivity ofΓ≤Γ′ It easily follows from the transitivity ofΓ⊢τ1≤τ2.◀ ▶Lemma 9.IfΘ|Γ⊢E[e] :τ⇒Γ′, then there existΓ1,τ′and freshzsuch that 1.Θ|Γ⊢e:τ′⇒Γ1 and 2.Θ|Γ1,z:τ′⊢E[z] :τ⇒Γ′. Proof. By induction onE...

  9. [9]

    3 is shown by Lemma 8

    Θ |Γ′,z:τ⊢z:τ⇒Γ′,z:τ′′whereτandτ′′havethesamesimpletypeandΓ |=Empty(τ′′) holds 5.(Γ ′,z:τ),τ≤Γ′,τ. 3 is shown by Lemma 8. 4 is derived by the rule T-Var. Here, we usedΓ,z:τ⊢τ+τ′′≈τ. It is easy to show thatΓ|=τ+τ′′≈τfor anyτandτ′′such that|τ|=|τ′′|andΓ |= Empty(τ′′) hold. 5 follows from definition of the relation≤betweenΓ′. The inductive case is the case w...

  10. [10]

    IfΘ |Γ⊢letx=nine :τ⇒Γ′, then there existΓ1 and τ′such that (1)Γ≤Γ1 and (2) Θ|Γ1,x:{ν:int|ν=n}⊢e:τ⇒(Γ′,x:τ′)

  11. [11]

    IfΘ |Γ⊢letx= null ine1 :τ⇒Γ′, then there existΓ1, τ1, andτ′such that (1)Γ≤Γ1, (2)Γ 1|=Empty(Πz.(τ0 refr)), (3)Θ|Γ1,x: Πz.(τ0 refr)⊢e1 :τ⇒(Γ′,x:τ′)

  12. [12]

    IfΘ |Γ⊢letx= y−zine: τ⇒Γ′, then there existΓ 1, φ, φ′, andτ′such that (1) Γ≤Γ1, (2)Γ 1(y) ={ν: int|φ}, (3)Γ 1(z) ={ν: int|φ′}, (4)Θ |Γ1,x:{ν: int|ν= y−z}⊢e:τ⇒(Γ′,x:τ′)

  13. [13]

    IfΘ |Γ⊢ifnpxthene0 elsee 1 :τ⇒Γ′, then there existΓ1, φthat satisfy (1)Γ≤Γ1, (2)Γ 1(x) ={ν: int|φ}, (3)Θ |Γ1 [x←↩{ν:int|φ∧ν≤0}]⊢e0 : τ⇒Γ′, and (4) Θ|Γ1 [x←↩{ν:int|φ∧ν >0}]⊢e1 :τ⇒Γ′,

  14. [14]

    IfΘ |Γ⊢letx= f(y1,...,y n) ine : τ′⇒Γ′, then there existΓ 1, x1, ..., xn, θ, τ1, ... τn, τ′ 1, ..., τ′ n, τ, and τ′′such that (1)Γ ≤Γ1, (2)Γ 1(yi) = θτi for1 ≤i≤n, (3)Θ( f) =⟨x1 :τ1,...,x n :τn⟩→⟨x1 :τ′ 1,...,x n :τ′ n|τ⟩, (4)θ= [y1/x1,...,y n/xn], (5) Θ|Γ1 [yi←↩θτ′ i],x:θτ⊢e:τ′⇒(Γ′,x:τ′′)

  15. [15]

    IfΘ |Γ⊢letx=e0 ine 1 :τ⇒Γ′, then there existΓ1,Γ 2 and τ′that satisfy (1)Γ≤Γ1, (2)Θ|Γ1⊢e0 :τ′⇒Γ2, and (3)Θ|Γ2,x:τ′⊢e1 :τ⇒(Γ′,x:τ′)

  16. [16]

    IfΘ |Γ⊢letx= allocy : int ref ine 0 : τ⇒Γ′, then there existΓ 1, τ′, φ, r, andz such that (1)Γ ≤Γ1, (2)Γ 1(y) ={ν: int|φ}, (3)Γ 1,z:int|= r = ((0 ≤z∧z≤ y−1)⇒1, 0), (4)Θ |Γ1,x: Πz.({ν: int|0≤z∧z≤y−1 =⇒ν= 0}refr)⊢e0 : τ⇒(Γ′,x:τ′)

  17. [17]

    IfΘ |Γ ⊢letx= allocy : (τ−ref) ref ine 0 : τ⇒Γ′, then there existΓ 1, φ, τ′, z, r, and τ′such that (1)Γ ≤Γ1, (2)Γ( y) = y:{ν: int|φ}, (3)Γ 1,z:int|= r = ((0 ≤z∧z≤y−1)⇒1, 0), (4)Γ 1,z:int|= Empty(τ′), (5)|τ′|= τ−ref, and (6) Θ|Γ1,x: Πz.(τ′refr)⊢e0 :τ⇒(Γ′,x:τ′)

  18. [18]

    IfΘ |Γ⊢letx=∗yine0 :τ⇒Γ′, then there existΓ1, z, τy, r, τ′,τ′′, τx, andτ′ y such that (1)Γ ≤Γ1, (2)Γ 1(y) = Πz.(τy refr), (3)Γ 1,z:{ν: int|ν= 0}⊢τ′+τx≈τy, (4) Γ1,x:τx,z:{ν: int|ν= 0}⊢τ′ y≈(τ′)=x, (5)Γ 1,x:τx,z:{ν: int|ν̸= 0}⊢τ′ y≈τy, 46 Ownership Refinement Types for Pointer Arithmetic and Nested Arrays (6)Γ 1,z:{ν: int|ν= 0}|= r > 0, and (7)Θ |Γ1 [ y←↩Πz...

  19. [19]

    IfΘ |Γ ⊢x: =y;e0 : τ⇒Γ′, then there existΓ 1, z, τ∗x, r, τ′ y, τ′, τy, τ∗x, and τ′ ∗xsuch that (1)Γ ≤Γ1, (2)Γ 1(x) = Π z.(τ∗xrefr), (3)Γ 1(y) = τy, (4)Γ 1,z:{ν: int|ν= 0} ⊢τ′ ∗x≈(τ′)=y, (5)Γ 1,z:{ν: int|ν̸= 0} ⊢τ′ ∗x≈τ∗x, (6)Θ | Γ1 [x←↩Πz.(τ′ ∗xrefr)] [ y←↩τ′ y ] ⊢e0 :τ⇒Γ′, (7)Γ 1,z:{ν: int|ν= 0}|=r =1, (8) Γ1⊢τ′ y +τ′≈τy

  20. [20]

    IfΘ |Γ ⊢letx= y⊞zine 0 : τ⇒Γ′, then there existΓ 1, w, τ3, τ′, ry, φ, rx, and ry1 such that (1)Γ ≤Γ1, (2)Γ 1(y) = Π w.(τ3 refry), (3)Γ 1(z) = {ν: int| φ}, (4)Γ 1 ⊢Πw.(τ1 refry1 ) + Π w.[(w−z)/w](τ2 refrx) ≈Πw.(τ3 refry)(5)Θ | Γ1 [y←↩Πw.(τ1 refry1 )],x: Πw.(τ2 refrx)⊢e0 :τ⇒(Γ′,x:τ′)

  21. [21]

    IfΘ |Γ⊢alias(x =y⊞z ) ;e 0 :τ⇒Γ′, then there existΓ1, w, τ∗x, rx, τ∗y, ry, rxz, r′xz, and r′x such that (1)Γ≤Γ1, (2)Γ 1(x) = Πw′.(τ∗xrefrx), (3)Γ 1(y) = Πw.(τ∗yrefry), (4)Γ 1(z) =z:{ν: int|φ}, (5)Γ 1⊢(Πw′.[(w′−z)/w′](τ∗xrefrx) + Πw.(τ∗yrefry))≈ (Πw′.[(w′−z)/w′](τ′ ∗xrefr′ x))+Πw.(τ′ ∗yrefr′ y)(6)Θ |Γ1 [ x←↩Πw.(τ′ ∗xrefr′ x) ][ y←↩Πw.(τ′ ∗yrefr′ y) ] ⊢ e0 :τ⇒Γ′

  22. [22]

    IfΘ |Γ ⊢alias(x =∗y) ;e 0 : τ⇒Γ′, then there existΓ 1, z, τ∗x, rx, w, τ∗∗y, r∗y, r, τ′ ∗x, r′x, and r′∗ysuch that (1)Γ ≤Γ1, (2)Γ 1(x) = Π z.(τ∗xrefrx), (3)Γ 1(y) = Πw.(Πz.(τ∗∗yrefr∗y) refr), (4)Γ1,w:{ν: int|ν= 0}⊢(Πz.(τ∗xrefrx)+Πz.(τ∗∗yrefr∗y))≈ (Πz.(τ′ ∗xrefr′ x) + Πz.(τ′ ∗∗yrefr′ ∗y)), (5)Γ 1,w:{ν: int|ν̸= 0}⊢Πz.(τ∗∗yrefr∗y)≈ Πz.(τ′ ∗∗yrefr′ ∗y), (6)Θ |...

  23. [23]

    Proof.We show only the proof of 2

    IfΘ |Γ⊢assert(φ) ;e 0 :τ⇒Γ′, then there existsΓ1 such that (1)Γ≤Γ1, (2)Γ 1|=φ and (3)Θ|Γ1⊢e0 :τ⇒Γ′. Proof.We show only the proof of 2. The other items are proved similarly. It must be the case that the judgmentΘ|Γ⊢letx=nine :τ⇒Γ′is derived by an application of T-Int, followed by zero or more applications ofT-Sub. Therefore, there exist Γ2,Γ 3,τ′′, andτ2 s...

  24. [24]

    Fujiwara, Y

    + own(H, R,v,τ′ 2)for Y. Fujiwara, Y. Matsushita, K. Suenaga and A. Igarashi 51 some τ′ 1,τ′ 2,r 1,r 2. The case wherev = null or v /∈dom(H)is trivial. Otherwise, v is the address(a,k)∈dom(H), satisfying own(H,R,(a,k),τ1) +own(H,R,(a,k),τ 2) = ∑ j∈Z {(a,k+j)↦→J[j/z]r1KR}+ ∑ j∈Z∧J[j/z]r1KR>0 own(H,R,H((a,k+j)),[j/z]τ ′ 1) + ∑ l∈Z {(a,k+j)↦→J[j/z]r2KR}+ ∑ j...

  25. [25]

    Thus,ConOwn(H,R{x′↦→R(y)},(Γ1,y:τ′ y,Γ 2,x′:τ′ x))holds. The proof of 2 From Lemma 27, it is sufficient to show the following: ConOwn(H,R{x′↦→H(R(y))},(Γ1,y: Πz.(τ′ y refr)ref r,Γ 2,x′:τx))holds if 1.ConOwn(H,R,(Γ 1,y: Πz.(τy refr),Γ 2)), 2.Γ 1,y: Πz.(τy refr),Γ 2,z:{ν:int|ν= 0}⊢τ′+τx≈τy, 3.Γ 1,y: Πz.(τy refr),Γ 2,x′:τx,z:{ν:int|ν= 0}⊢τ′ y≈(τ′)=x′ , 4.Γ 1...

  26. [26]

    Γ1,z 2 :{ν: int|ν= 0}⊢(Πz′ 1.(τ∗xrefrx) + Πz1.(τ∗∗yrefr∗y))≈(Πz′ 1.(τ′ ∗xrefr′ x) + Πz 1.(τ′ ∗∗yrefr′ ∗y))and 5.Γ 1,z 2 :{ν:int|ν̸= 0}⊢Πz1.(τ∗∗yrefr)∗y≈Πz1.(τ′ ∗∗yrefr′ )∗yand 6.H(R(y)) =R(x). Y. Fujiwara, Y. Matsushita, K. Suenaga and A. Igarashi 59 LetΓ ′be(Γ 1 [ x←↩Πz′ 1.(τ′ ∗xrefr′ x) ][ y←↩Πz2.(Πz1.(τ′ ∗∗yrefr′ ∗y)ref r) ] ). Since only the types ofx...

  27. [27]

    Since only the types ofx and ydiffer betweenΓ 1 andΓ ′, we will consider theownofxandy

    Γ1⊢(Πw′.[(w′−z)/w′](τ∗xrefrx)+Πw.(τ∗yrefry))≈(Πw′.[(w′−z)/w′](τ′ ∗xrefr′ x))+ Πw.(τ′ ∗yrefr′ y) LetΓ ′be(Γ 1 [ x←↩Πw′.(τ′ ∗xrefr′ x) ][ y←↩Πw.(τ′ ∗∗yrefry) ] ). Since only the types ofx and ydiffer betweenΓ 1 andΓ ′, we will consider theownofxandy. own(H,R,pv⊞R(z),Πw ′.(τ′ ∗xrefr′ x)) +own(H,R,pv,Πw.(τ′ ∗yrefr′ y)) =own(H,R,pv,Πw ′.[(w′−z)/w′](τ′ ∗xrefr′ ...

  28. [28]

    Whenv = null, this is straightforward

    ⇐⇒ SA T v(H, R,v,τ′ 3)for some τ′ 1,τ′ 2,τ′ 3,r 1,r 2,r 3. Whenv = null, this is straightforward. We consider the case wherev̸=null. SA T v(H,R,v,τ1)∧SA T v(H,R,v,τ2)⇐=SA T v(H,R,v,τ3)direction Y. Fujiwara, Y. Matsushita, K. Suenaga and A. Igarashi 63 AssumeSA T v(H,R,(a,k),Πz.(τ′ 3 refr3))for some address(a,k). SA T v(H,R,(a,k),Πz.(τ′ 3 ref 3)) ⇐⇒ ∀j.J[j...

  29. [29]

    IfΓ ≤Γ1,y: Πz.(τ′ y refr), Γ2,x′:τx and SA T(H, R, Γ1,y: Πz.(τy refr), Γ2),(Γ 1,y: Πz.(τy refr), Γ2,z:{ν: int|ν= 0})⊢τ′+τx≈τy,(Γ 1,y: Πz.(τy refr), Γ2,x′:τx,z:{ν: int|ν= 0})⊢ τ′ y ≈(τ′)=x′ ,(Γ 1,y: Πz.(τy refr), Γ2,x′:τx,z:{ν: int|ν̸= 0}) ⊢τ′ y ≈τy, x′/∈ dom(Γ1,y: Πz.(τy refr), Γ2)∪dom(R),R(y) = (a,i )∈dom(H)andΓ 1,y: Πz.(τy refr), Γ2,z:{ν: int|ν= 0}|=r >...

  30. [30]

    LetΓ ′beΓ 1 [ x←↩Πz.(τ′ ∗xrefr′ x) ][ y←↩Πw.(Πz.(τ′ ∗∗yrefr′ ∗y)ref r) ]

    Γ,w:{ν: int|ν= 0}⊢(Πz.(τ∗xrefrx) + Πz.(τ∗∗yrefr∗y))≈(Πz.(τ′ ∗xrefr′ x) + Πz.(τ′ ∗∗yrefr′ ∗y))and 5.Γ,w:{ν:int|ν̸= 0}⊢Πz.(τ∗∗yrefr∗y)≈Πz.(τ′ ∗∗yrefr′ ∗y)and 6.H(R(y)) =R(x). LetΓ ′beΓ 1 [ x←↩Πz.(τ′ ∗xrefr′ x) ][ y←↩Πw.(Πz.(τ′ ∗∗yrefr′ ∗y)ref r) ] . Since only the types ofx andy differ betweenΓandΓ ′, we will consider theSA T vofx andy. WhenR(y) = null, we ...

  31. [31]

    Since only the types ofx and y Y

    Γ⊢(Πw′.[(w′−z)/w′](τ∗xrefrx)+Π w.(τ∗yrefry))≈(Πw′.[(w′−z)/w′](τ′ ∗xrefr′ x))+ Πw.(τ′ ∗yrefr′ y) LetΓ′beΓ 1 [ x←↩Πw′.(τ′ ∗xrefr′ x) ][ y←↩Πw.(τ′ ∗yrefr′ y) ] . Since only the types ofx and y Y. Fujiwara, Y. Matsushita, K. Suenaga and A. Igarashi 71 differ betweenΓandΓ ′, we will consider theSA T vofxandy. SA T v(H,R,R(x),Γ 1(x))∧SA T v(H,R,R(y),Γ1(y)) ⇐⇒SA...