Dependent-Type-Preserving Memory Allocation

Paulette Koronkevich; William J. Bowman

REVIEW 4 major objections 4 minor 6 references

Dependent-Type-Preserving Memory Allocation

T0 review · 4 major / 4 minor · reviewed 2026-08-04 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read A compiler pass allocates memory without erasing dependent types, so linked code can be checked against the original specification.

desk verdict Sensible ongoing-work report with a real gap: the Pi/closure type translation is missing, so the main theorem is not checkable as stated. read the letter →

arxiv 2509.09059 v1 pith:5SR76KAN submitted 2025-09-10 cs.PL

Paulette Koronkevich , William J. Bowman This is my paper · ORCID

classification cs.PL

keywords dependenttypestype-preservingcompilationmemoryallocationinitializationflagsclosureconversiontypedintermediatelanguagelinkingcompilercorrectness

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

Most dependently typed languages erase specifications during compilation, so a later-linked C program can break them—for example, by passing an uninitialized pointer into the compiled code. The paper's proposal is to keep specifications alive by making memory allocation a typed operation rather than an untyped runtime effect. It defines a target language, CC-CC_A, whose dependent pair types carry initialization flags and which has explicit malloc and field-assignment operators. It then defines a translation from CC-CC and claims that every well-typed source term translates to a well-typed target term (Theorem 3.1). If the claim holds, this is a step toward a dependent-type-preserving compiler where link-time type checking can reject ill-typed external code.

What carries the argument

The mechanism that carries the argument is the initialization-flag dependent pair type, written 𝚺x:A^𝝓.B^𝝓' in the target language. The flags record whether each component of the pair has been initialized: malloc produces a pair with both flags 0, each field-assignment flips the corresponding flag, and projection rules require the flag to be 1. The translation J·K turns every source pair or closure value into a let-sequenced malloc followed by two field writes, so the resulting term's type itself records that both fields are initialized. This is what makes uninitialized-memory errors ill-typed rather than something to be caught at runtime.

What would settle it

Check whether the manuscript defines the translation for the dependent function type Πx:A.B and the code type Code(x:A,x':A').B. Figure 2 shows the translation of closure values but not of their types. If that clause is absent, Theorem 3.1 has no target type for any source program that uses a function, so the central claim as stated would collapse; a reader can decide this by looking for the omitted clause. As a second test, attempt the induction step of Lemma 3.5 for the case where the substituted variable appears in the type of a dependent pair; the translation introduces flag annotations th

Watch

Extended reading notes

Core claim

The paper's central claim is a translation J·K that compiles every source pair into an allocation sequence: allocate a two-word tuple, write both fields, and return the tuple with its type flags set to initialized; closures are allocated the same way then tagged as Clos. The target type system's key rule [Clo] lets a fully initialized allocated pair be used as a dependent function type. The paper states that this translation is type-preserving—the empty target context proves JΓK⊢JeK:JAK whenever Γ⊢e:A—and that this follows by straightforward induction from preserved subtyping, equivalence, conversion, and substitution lemmas. It also sketches a consistency argument for CC-CC_A by modelling i

Load-bearing premise

The theorem rests on the unstated conversion relation of the target language and on the unproved Lemma 3.5, that the allocation translation commutes with substitution on terms whose types mention dependent pairs; if either gives way, the type-preservation proof cannot be completed.

Editorial extensions

If this is right

If correct, the pass lets compiler writers keep dependent specifications across allocation, so link-time type checking can prevent linking with code that violates memory-safety specifications.
The pass is designed to slot between existing typed CPS and closure-conversion passes, moving the compiler closer to a certified dependent-type-preserving pipeline to C.
The initialization flags make projections from uninitialized pairs statically impossible, eliminating a whole class of use-before-initialize bugs.
Completing the eCIC model would give a consistency proof for CC-CC_A, ensuring the target language cannot be used to prove false.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

The flag discipline is a lightweight form of permission tracking; one could generalize it to linear kinds and use it to type-check region-based memory management or a GC interface, a connection the paper does not draw.
The approach should transfer to any phase where initialization order matters—I/O buffers, GPU uploads, protocol serialisers—where dependent pair types with initialization flags could statically prevent use-before-write bugs.
A direct test would be to formalize Lemmas 3.2–3.5 in a proof assistant; the paper's 'straightforward induction' claim is not the same as a checked proof, and the omitted closure-type clause would force the formalizer to state it explicitly.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

The core idea here is sound and worth engaging with: take the initialization-flag trick from Morrisett et al., adapt it to dependent pair types, and use it for a type-preserving allocation pass on Bowman and Ahmed's CC-CC. That combination hasn't appeared before, and the motivating problem—checked linking against external code that could hand you uninitialized memory—is genuine. The translation in Figure 2 is clean: malloc, initialize components one at a time, tag closures. It reads like a natural next step in a longer dependent-type-preserving compiler project.

The paper is also honest about what is done and what is not. Section 4 explicitly says the eCIC model is ongoing, and the main theorem is presented as a proof sketch. That is the right framing for ongoing work.

But the stress-test is on target. Theorem 3.1 quantifies over all source types A, and CC-CC includes dependent functions and closure types, yet Figure 2 gives no translation for Π x:A.B, Code(...), or universes. The closure case literally produces a Clos tag, but without knowing what JΠ x:A.BK is, you cannot check the type preservation claim for closures—which is supposedly a central target of the pass. This is not a minor omission; it is the difference between a theorem statement and a precise one.

Also, the proof relies on Lemmas 3.3–3.5, all stated without proof. Lemma 3.5 (substitution preservation) is especially load-bearing: with heap allocation and flag changes, Je[e'/x]K should definitionally equal JeK[Je'K/x], but allocation order and local bindings could easily break that. The claim that everything follows by "straightforward induction" is too casual for this setting.

To be fair: I do not see a fatal flaw. The design is plausible, the prior work is cited appropriately, and the paper's own warnings align with my reading. The missing pieces are exactly what an extended abstract would defer, but they are too big for the theorem as stated to be verified.

Who is this for? People working on type-preserving compilation for dependently typed languages. A workshop or a short-paper referee should look at it seriously; it will not be a full conference paper until the translation is completed and the lemmas are proved. I would bring it to a reading group, and I would cite it if I worked in this area. Recommendation: send to peer review, but expect revision or a more limited claim.

Referee Report

4 major / 4 minor

Summary. The paper presents an ongoing design for a typed intermediate language CC-CC_A that adds explicit memory allocation and initialization to the dependently typed language CC-CC. The main contribution is a compiler pass, described in Figure 2, that translates dependent pairs and closures from CC-CC into CC-CC_A programs that allocate heap cells, initialize them, and (in the closure case) tag them as closures. The central claimed theorem (Theorem 3.1) states that this pass is type-preserving: if Γ ⊢ e : A in CC-CC, then ·; JΓK ⊢ JeK : JAK in CC-CC_A. The paper also sketches a consistency argument for CC-CC_A via a translation into extensional CIC. The proof of Theorem 3.1 is not supplied; it is asserted to follow by induction using Lemmas 3.2–3.5, which are also stated without proof. Section 4 explicitly notes that the eCIC model proof is still ongoing.

Significance. If completed, this work would provide a important building block for a fully dependently typed end-to-end compiler, addressing a real gap: linking trusted external code against erased specifications. The design of a dependent pair type with initialization flags, and the idea of treating closure allocation as heap initialization, are plausible and of interest to the PL/compiler community. The paper does not currently supply machine-checked proofs, complete definitions, or a verified consistency argument; its value is at the design/vision stage. The central theorem is not yet checkable because key definitions and lemmas are missing.

major comments (4)

[Section 2, Figure 2] The allocation translation is defined only for Σ types, pairs, and closures. There is no equation for JΠ x:A.BK, JCode(...)K, or the universes. Since Theorem 3.1 quantifies over all source types A, and since the source calculus includes dependent function types and code types, the statement of the theorem is incomplete. In particular, the closure case in Figure 2 produces `Clos y2`, and its typing requires knowing JΠ x:A.BK to conclude that the translated term has the claimed type. The missing Π-type clause is load-bearing: without it, the closure case of Theorem 3.1 cannot even be stated, let alone proved.
[Section 3, Lemmas 3.3–3.5] Lemmas 3.3, 3.4, and 3.5 are stated without proof. Lemma 3.5 (substitution preservation) is especially nontrivial and load-bearing: the translation introduces let-bindings, malloc, and initialization flags, so Je[e'/x]K and JeK[Je'K/x] may differ in allocation order, local let-bindings, and flag states. This lemma is required by the [Snd] rule and by the closure case of Theorem 3.1, where a term is substituted into a type. Lemma 3.4 also needs to account for the extra allocation and initialization steps in the translated program and for the heap (the conclusion mentions an arbitrary heap Ψ, but no typing rule for heaps is given). The assertion that these lemmas follow by 'straightforward induction' is not sufficient for a dependency-typed setting with a mutable heap.
[Section 4] The consistency of the target language CC-CC_A is explicitly left as ongoing work. The paper claims that the eCIC model 'should be type-preserving' but does not provide the proof. Since a central motivation of the work is to ensure that linked external code cannot violate specifications, the type preservation theorem alone is insufficient: if CC-CC_A is inconsistent, then it could prove false, and the safety guarantee from typing would be vacuous. This is not a demonstrated flaw, but it is a missing load-bearing part of the overall claim.
[Section 3, Theorem 3.1] The theorem states `·; JΓK⊢ JeK : JAK`, but no definition of JΓK is given in Figure 2 or the surrounding text. Context translation is not trivial: variables now range over heap locations, and the context must account for the types of allocated pairs. The proof of the theorem cannot be checked without this definition. This is a small but necessary missing piece of the central statement.

minor comments (4)

[Section 2, Figure 1] The [Clo] rule has a layout issue: the premise `e : Σ y:(Code(x1:A1, x:A).B) 1. A1^1` and the conclusion `Clos e : Π x:A[snd e/x1].B[snd e/x1]` are printed with unusual superscripts and spacing. These should be typeset more clearly, and the precise flag annotations should be explained.
[Section 4] Typo: 'readibility' should be 'readability'.
[Section 2] The paper says the typing/subtyping/conversion rules for CC-CC are 'the same as given by Bowman and Ahmed [3]' but does not reproduce them. Since CC-CC is not a standard calculus and the target rules depend on the source's conversion relation, a reader cannot verify the claims without consulting the external paper. A brief appendix recalling the source rules would improve self-containedness.
[Section 2, CC-CC_A syntax] The syntax of CC-CC_A is not given as a grammar; the text only mentions extensions. A formal syntax summary would help clarify the distinction between locations, heap values, and source expressions.

Circularity Check

0 steps flagged · score 1.0 of 10

No circular derivation; theorem is under-specified and has unproved lemmas, but the translation is not fitted or self-referential.

full rationale

The allocation pass is a syntactic translation defined by recursion over CC-CC expressions and types (Figure 2), and CC-CC_A is a separately defined target language with its own typing rules (Figure 1). The correctness claim, Theorem 3.1, is a standard type-preservation statement; its proof would be an induction over the source typing derivation. Nothing in the paper fits a parameter to data, renames a known empirical result, or imports a uniqueness theorem from the authors' prior work. The source calculus CC-CC is taken from the previously published PLDI 2018 paper by Bowman and Ahmed [3], which includes one author of the present work, but that citation supplies the source language's typing/conversion rules rather than the target-language typing rules or the translation's correctness; it is not a self-citation chain that substitutes for the proof. The target typing rules [Malloc], [Assign1], [Assign2], [Fst], [Snd], and [Clo] are new in this paper, and the closure-tagging rule is not derived from a self-citation. The manuscript does, however, flag its own incompleteness: Section 4 says the eCIC consistency model is 'still ongoing,' and Section 3 states Lemmas 3.2-3.5 and Theorem 3.1 are proved by 'straightforward induction' without giving the proof. Figure 2 omits the translation of dependent function/closure types (JΠ x:A.BK), Code types, and universes, even though Theorem 3.1 quantifies over all source types; the closure case produces Clos y2 and relies on [Clo], whose conclusion involves substitutions [snd e/x1], so without JΠ x:A.BK the theorem is not checkable for closures. Lemma 3.5 (Je[e'/x]K ≡ JeK[Je'K/x]) is load-bearing for dependent elimination and could be nontrivial with allocation order and initialization flags. These are serious correctness gaps, but they are omissions, not circular reductions. Accordingly the circularity score is low.

Assumptions & free parameters 0 free parameters · 4 assumptions · 2 invented entities

The central claim rests on the source calculus from [3], an unstated conversion relation for the target, an incomplete translation definition, and an unfinished eCIC model. No numerical parameters are fitted; the introduced constructs are language design elements, not empirically evidenced entities.

assumptions (4)

domain assumption CC-CC typing, subtyping, and conversion rules are exactly as in Bowman and Ahmed [3].
The paper does not restate the source calculus's rules; Theorem 3.1 inherits any hidden assumptions or bugs in [3].
ad hoc to paper The conversion relation of CC-CC_A over configurations with heaps exists and supports the stated lemmas.
The paper defines only excerpts of reduction for projection; the full conversion relation is not specified, yet Lemmas 3.3-3.5 rely on it.
ad hoc to paper The allocation translation extends to all source typing derivations, including dependent function types, despite only pair and closure cases being shown.
The translation of types such as Pi and Code is not given; Theorem 3.1 assumes these cases are handled and type-preserving.
ad hoc to paper The eCIC model translation is type-preserving.
Section 4 states this proof is ongoing; the consistency claim for CC-CC_A is therefore not yet established.

invented entities (2)

Initialization flag phi on dependent pair types
purpose: Mark whether heap-allocated pair components are initialized to prevent projections from reading uninitialized memory.
Introduced in CC-CC_A; derived from Morrisett et al. [5], not independently evidenced here.
Clos tagging operator
purpose: Marks an initialized pair of code and environment as a closure value of dependent function type.
New operator in CC-CC_A; its typing rule [Clo] is asserted without a semantic model or proof.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Dependent-Type-Preserving Memory Allocation." pith.science (2026). https://pith.science/paper/5SR76KAN

@misc{pith2026250909059,
  author       = {Pith},
  title        = {Pith review of: Dependent-Type-Preserving Memory Allocation},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/5SR76KAN}},
  note         = {Machine review of arXiv:2509.09059}
}

read the original abstract

Dependently typed programming languages such as Coq, Agda, Idris, and F*, allow programmers to write detailed specifications of their programs and prove their programs meet these specifications. However, these specifications can be violated during compilation since they are erased after type checking. External programs linked with the compiled program can violate the specifications of the original program and change the behavior of the compiled program -- even when compiled with a verified compiler. For example, since Coq does not allow explicitly allocating memory, a programmer might link their Coq program with a C program that can allocate memory. Even if the Coq program is compiled with a verified compiler, the external C program can still violate the memory-safe specification of the Coq program by providing an uninitialized pointer to memory. This error could be ruled out by type checking in a language expressive enough to indicate whether memory is initialized versus uninitialized. Linking with a program with an uninitialized pointer could be considered ill-typed, and our linking process could prevent linking with ill-typed programs. To facilitate type checking during linking, we can use type-preserving compilation, which preserves the types through the compilation process. In this ongoing work, we develop a typed intermediate language that supports dependent memory allocation, as well as a dependent-type-preserving compiler pass for memory allocation.

Figures

Figures reproduced from arXiv: 2509.09059 by the authors.

**Figure 1.** CC-CC𝐴 Typing (excerpt) JeK = e JΣ x : A. BK def = 𝚺 x : JAK 1 . JBK 1 J⟨e1, e2⟩ as Σ x : A. BK def = let y = mallocx [JAK , JBK] : 𝚺 x : JAK 0 . JBK 0 in let y1 = y[1]←Je1K : 𝚺 x : JAK 1 . JBK 0 in let y2 = y1 [2]←Je2K : 𝚺 x : JAK 1 . JBK 1 in y2 J⟨⟨e1, e2⟩⟩ as Π x : A. BK def = let y = mallocx [JCode (x ′ : A1, x : A). BK , JA1K] in let y1 = y[1]←Je1K : 𝚺 x : JCode (x ′ : A1, x : A). BK 1 . A 0 1 in let y2 = y1 [2… view at source ↗

**Figure 2.** Allocation Translation (excerpt) The typing rules for CC-CC𝐴 remain mostly the same as CC-CC; however, we now include the heap while type checking to access tuples that have been allocated. The heap 𝚿 consists of locations with their types ℓ : A as well as locations mapped to heap values ℓ ↦→ ⟨e1, e2⟩. Small step reduction ▷ and conversion ▷ ∗ are defined over configurations ⟨𝚿 | e⟩ to access the allocated tuples. F… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

6 extracted references · 1 canonical work pages

[1]

Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Bélanger, Matthieu Sozeau, and Matthew Weaver

Abhishek Anand, Andrew W. Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Bélanger, Matthieu Sozeau, and Matthew Weaver. 2017. CertiCoq: A verified compiler for Coq. InInternational Workshop on Coq for Programming Languages (CoqPL). http://www.cs.princeton.edu/~appel/papers/certicoq-coqpl.pdf

2017
[2]

Simon Boulier, Pierre-Marie Pédrot, and Nicolas Tabareau. 2017. The Next 700 Syntactical Models of Type Theory. In Conference on Certified Programs and Proofs (CPP). doi:10.1145/3018610.3018620

arXiv 2017
[3]

Bowman and Amal Ahmed

William J. Bowman and Amal Ahmed. 2018. Typed Closure Conversion for the Calculus of Constructions. InInternational Conference on Programming Language Design and Implementation (PLDI). doi:10.1145/3192366.3192372

arXiv 2018
[4]

Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed

William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed. 2018. Type-preserving CPS Translation of Σ and Π Types Is Not Not Possible.Proceedings of the ACM on Programming Languages (PACMPL)2, POPL (Jan. 2018). doi:10.1145/3158110

work page doi:10.1145/3158110 2018
[5]

Greg Morrisett, David Walker, Karl Crary, and Neal Glew. 1999. From System F to Typed Assembly Language.ACM Transactions on Programming Languages and Systems (TOPLAS)21, 3 (May 1999). doi:10.1145/319301.319345

arXiv 1999
[6]

Aleksandar Nanevski, Greg Morrisett, and Lars Birkedal. 2006. Polymorphism and Separation in Hoare Type Theory. In International Conference on Functional Programming (ICFP). doi:10.1145/1159803.1159812

arXiv 2006

Pith tools

Reviewed August 4, 2026 · model on record in the stance chip above.

[1] [1]

Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Bélanger, Matthieu Sozeau, and Matthew Weaver

Abhishek Anand, Andrew W. Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Bélanger, Matthieu Sozeau, and Matthew Weaver. 2017. CertiCoq: A verified compiler for Coq. InInternational Workshop on Coq for Programming Languages (CoqPL). http://www.cs.princeton.edu/~appel/papers/certicoq-coqpl.pdf

2017

[2] [2]

Simon Boulier, Pierre-Marie Pédrot, and Nicolas Tabareau. 2017. The Next 700 Syntactical Models of Type Theory. In Conference on Certified Programs and Proofs (CPP). doi:10.1145/3018610.3018620

arXiv 2017

[3] [3]

Bowman and Amal Ahmed

William J. Bowman and Amal Ahmed. 2018. Typed Closure Conversion for the Calculus of Constructions. InInternational Conference on Programming Language Design and Implementation (PLDI). doi:10.1145/3192366.3192372

arXiv 2018

[4] [4]

Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed

William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed. 2018. Type-preserving CPS Translation of Σ and Π Types Is Not Not Possible.Proceedings of the ACM on Programming Languages (PACMPL)2, POPL (Jan. 2018). doi:10.1145/3158110

work page doi:10.1145/3158110 2018

[5] [5]

Greg Morrisett, David Walker, Karl Crary, and Neal Glew. 1999. From System F to Typed Assembly Language.ACM Transactions on Programming Languages and Systems (TOPLAS)21, 3 (May 1999). doi:10.1145/319301.319345

arXiv 1999

[6] [6]

Aleksandar Nanevski, Greg Morrisett, and Lars Birkedal. 2006. Polymorphism and Separation in Hoare Type Theory. In International Conference on Functional Programming (ICFP). doi:10.1145/1159803.1159812

arXiv 2006