{"id":"f83c6257-aa1b-4596-9794-b026a7b1dc7d","arxiv_id":"1908.02035","paper_version":3,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A dependently typed multi-stage calculus with quasi-quotation, escape, run, and cross-stage persistence is defined and proven to enjoy preservation, strong normalization, confluence, and progress.","lead":"λMD is a new calculus that adds dependent types to multi-stage programming, so a program can generate code whose type records properties such as vector length. The paper proves that the calculus is type-safe and terminating, and demonstrates how cross-stage persistence is key to writing dependently typed code generators.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Section 2.2's claim that Vector x is not well-formed at stage α under x:Int@ε is contradicted by the formal K-Csp rule, which derives exactly that judgment.","rationale":"The reader's weakest assumption identified the same internal inconsistency between Section 2.2 and the formal K-Csp rule, and my independent reading confirms it is the most load-bearing concern. The central claim of the paper has two parts: the definition of λMD and the proof of its metatheoretic properties. The metatheorem proofs are sketched and contain gaps (e.g., the confluence theorem is stated for all terms but proved via Newman's Lemma using strong normalization only for typed terms; the value grammar omits constants and Unique Decomposition omits the T-Const case), but these are likely fixable with standard arguments. The K-Csp inconsistency is different: it undermines the paper's core motivation for term-level CSP and the Q-% equivalence, because the formal rules already provide the type-level lifting that Section 2.2 claims is impossible. This is a substantive design-level contradiction, not a proof gap. The paper can likely be repaired by either constraining K-Csp (e.g., requiring the type to be closed or to have indices available at the target stage) or by rewriting Section 2.2 and the significance argument to match the more permissive formal system, but as written the central narrative is not coherent. The reader's CONDITIONAL verdict is therefore appropriate; I do not see grounds to move it to ACCEPT or REJECT without the authors' clarification, so I recommend UNCHANGED.","tokens_in":24506,"tokens_out":20414,"duration_ms":205918,"concrete_test":"Construct the full derivation of x:Int@ε ⊢Σ Vector x :: ∗@α using exactly the printed rules K-TConst, T-Var, K-App, and K-Csp from Section 3.3/Appendix A.3. If the derivation is valid (inspection says it is), then Section 2.2's motivating assertion is false. A sharper follow-up: remove K-Csp from the system and re-check whether the motivating example λx:Int.◮α(λy:Vector x.M) is rejected and whether the stated metatheorems (preservation, SN, confluence, progress) still hold, to determine whether the formal system's actual design matches the paper's stated motivation.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's motivating example hinges on the assertion in Section 2.2 that, with x:Int@ε, the type Vector x is well-formed at ε but not at α, so term-level CSP (%αx) is needed to express the type inside a quotation. However, the formal kinding rules in Section 3.3 include K-Csp: Γ ⊢Σ τ :: ∗@A implies Γ ⊢Σ τ :: ∗@Aα, with no side condition on free term variables or stages. From Vector :: Πx:Int.∗ (K-TConst), x:Int@ε (T-Var), and K-App, we can derive x:Int@ε ⊢Σ Vector x :: ∗@ε. Applying K-Csp with A=ε and α gives x:Int@ε ⊢Σ Vector x :: ∗@α. Thus the very judgment Section 2.2 claims is underivable is derivable. This is not a mere typo: it means the formal system already provides implicit type-level CSP for arbitrary open types, so the claimed necessity of term-level CSP for the vector-size example is not established. If K-Csp is intended, Section 2.2 must be rewritten; if the intended design was to restrict type well-formedness to the stages of index terms, K-Csp must be constrained or removed. As written, the informal overview and the formal definition contradict each other, weakening the paper's central argument about the significance of cross-stage persistence in dependently typed multi-stage programming.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces λMD, a calculus that extends Hanada and Igarashi's λ⊲% with LF-style dependent types. The calculus supports quasi-quotation ◮α, escape ◭α, stage abstraction Λα with application to stage sequences, run represented as application to ε, and cross-stage persistence %α; types are classified by kinds and equipped with congruences and special equivalences, with stages attached to typing, kinding, and equivalence judgments. The authors define full reduction and a staged small-step call-by-value semantics, state term and stage substitution lemmas and inversion lemmas, and claim preservation, strong normalization, and confluence for full reduction as well as unique decomposition and progress for staged reduction. The appendix gives the complete rule set and proof sketches, and a vector-addition example is used to motivate term-level CSP in type indices.","tokens_in":24755,"tokens_out":16005,"duration_ms":217955,"significance":"If the metatheorems hold, λMD is a useful first step toward a formal account of full-spectrum dependent types in MetaOCaml-style staging, and the paper identifies a genuine design question: how stages should interact with type well-formedness. The paper is explicit that typechecking, residualization, and detailed proofs are left to future work. Its strength is the concrete formal system and the erasure-based normalization strategy; the proofs are not machine-checked. However, the formal rule K-Csp contradicts the motivating discussion, and the strong-normalization proof contains a false claim about the size behavior of Λ-reduction. These issues do not, on my reading, invalidate the whole formal system, but they do mean that the central presentation and one load-bearing proof argument need substantial repair before the paper is publishable.","major_comments":[{"comment":"The informal overview and the formal kinding rules are contradictory. Section 2.2 states that under x:Int@ε the type Vector x is well-formed at ε but not at α, and uses this to argue that λx:Int.◮α(λy:Vector x.M) is rejected without term-level CSP, so that Vector (%αx) is needed. However, K-Csp in Section 3.3 (and Appendix A.3) has no side condition and derives Γ ⊢Σ τ :: ∗@Aα from Γ ⊢Σ τ :: ∗@A. With Vector :: Πx:Int.∗ in the signature, K-TConst and K-App give x:Int@ε ⊢Σ Vector x :: ∗@ε, and one application of K-Csp with A = ε gives x:Int@ε ⊢Σ Vector x :: ∗@α. The type Vector x is therefore already legal at stage α, and the generator λx:Int.◮α(λy:Vector x.M) is typeable without %αx. The paper must either constrain or remove K-Csp (while preserving the matrix-type example in Section 3.3) or rewrite Section 2.2 so that implicit type-level CSP is presented as the lifting mechanism, with term-level CSP motivated only by index terms that genuinely live at different stages. As written, the paper's central motivation for term-level CSP in dependent types is not established.","section":"Section 2.2 / Section 3.3 (K-Csp)"},{"comment":"The strong-normalization argument contains a false premise. The proof states: 'If there is an infinite reduction sequence in λMD then there are infinite beta reductions in the sequence. This is because reductions other than β-reduction reduce the size of a term.' Λ-reduction does not always reduce size: for example, (Λα.◮α◮αx) βγ reduces to ◮β◮γ◮β◮γx, which is syntactically larger. Thus the claim that any infinite sequence must contain infinitely many β-reductions is unsupported. The erasure proof needs a separate, correct argument that ◆- and Λ-reductions terminate (for instance, a well-founded measure on stage redexes), or an alternative normalization proof.","section":"Appendix, proof of Theorem 10"}],"minor_comments":[{"comment":"Item 3 of Lemma 3 contains a typo: 'there is σ such that σ = ∀α.σ' should read 'there is σ such that τ = ∀α.σ'.","section":"Section 4, Lemma 3"},{"comment":"The type case of the erasure is written ♮(τ x) = ♮(τ), but the syntax of types has arbitrary term applications τ M; the case should quantify over all M. Also, the context case ♮(Γ, X : K@A) refers to a form that is not in the grammar of Γ and should be removed or corrected.","section":"Appendix B, Definition 1 (♮ translation)"},{"comment":"Lemma 15 is stated as 'If Γ ⊢Σ M : τ @A and M −→β N in λMD then ♮(M) = ♮(N)', but the lemma is about Λ-reduction; the subscript should be Λ.","section":"Appendix B, Lemma 15"},{"comment":"The weak Church–Rosser justification is incomplete: for two redexes where one is inside the body of another, reducing the outer redex can duplicate the inner redex, so the sentence 'we can reduce one of them after we reduce another' is not by itself a proof. Please spell out the standard argument or cite a lemma covering this case.","section":"Appendix, Theorem 11"}],"recommendation":"major_revision","confidential_remarks":"The manuscript is within the journal's scope and the related-work discussion is fair. The main editorial risk is that the K-Csp contradiction may tempt the authors to remove K-Csp, which would change the calculus and could invalidate the examples and metatheorems; the editor should ensure that the revised version re-checks the proofs against the final rule set. I do not see a novelty-disclosure problem."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Let me skip the throat-clearing. This is a genuine step forward: λMD appears to be the first formal calculus that puts full-spectrum dependent types together with quasi-quotation, escape, run-as-stage-application, and cross-stage persistence, and the paper proves the standard package (preservation, confluence, SN, progress) with an erasure-based SN argument that is likely sound. The definitions are careful, and the choice of λLF as the dependent base is sensible. The novelty claim over the cited prior work (λH◦, Concoqtion, Brady-Hammond) looks supported.\n\nThe soft spot is real and not minor. Section 2.2 says that with x : Int@ε, the type Vector x is well-formed at ε but not at α, and uses that to motivate term-level CSP. But the formal K-Csp rule in Section 3.3 derives exactly the judgment x : Int@ε ⊢ Vector x :: ∗@α, with no side condition on free term variables. The stress-test note is correct. This is a contradiction between the informal overview and the formal system, and it weakens the paper's central motivating example. The calculus may still be coherent; the fix is either to constrain K-Csp (so implicit type-level CSP only applies to closed types or types whose index terms are stage-flexible) or to rewrite Section 2.2 to say that implicit CSP already lifts open types, and term-level CSP is needed when a type constructor takes arguments from different stages (which the authors themselves note in the remark after the example). As written, the two parts of the paper disagree, and a reader cannot tell which is intended.\n\nThere are smaller issues. Lemma 3 has a typo in the Λ-inversion case (σ = ∀α.σ should presumably be τ = ∀α.σ). The appendix proofs are sketches; representative cases are given but many are dispatched as “straightforward induction.” For this kind of paper that is contestable but not fatal, since the cases really do look routine. The Q-% rule is interesting and well rationalized.\n\nOverall: the formal contribution is solid enough to warrant serious refereeing. The contradiction is in the exposition and the motivation, not obviously in the metatheory, but it needs to be resolved before the paper can be accepted. I would send it to a good PL venue and let the referees push on the K-Csp rule.","headline":"Real first formal combination of dependent types with MetaOCaml-style staging, but the paper's own motivating example contradicts its formal K-Csp rule.","tokens_in":25338,"tokens_out":2960,"would_cite":true,"duration_ms":29781,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper develops λMD, a dependently typed multi-stage calculus, and proves type soundness, strong normalization, confluence, and progress.","keywords":["multi-stage programming","dependent types","cross-stage persistence","quasi-quotation","type preservation","strong normalization","confluence","staged reduction"],"falsifier":"Check the derivability of the judgment x:Int@ε ⊢Σ Vector x :: ∗@α: if a formalization of the rules derives it via K-Csp while Section 2.2 claims it is not well-formed, then either the rules or the motivating example must change, and until that is settled the metatheorems cannot be taken as applying to the intended system. A proof assistant can settle this directly by attempting to construct or refute that derivation.","tokens_in":24267,"feed_emoji":"🔧","tokens_out":9982,"duration_ms":94571,"temperature":0.7,"pith_summary":"Multi-stage programming lets programs build and run code at run time; dependent types let types mention values, such as the length of a vector. The paper asks whether the two can be combined without losing safety and shows that the answer is yes by defining λMD, an extension of the multi-stage calculus λ⊲% with dependent function types, code types indexed by stages, and cross-stage persistence at both term and type level. The paper proves preservation, strong normalization, and confluence for full reduction, and progress for staged call-by-value evaluation. If these results are correct, λMD is the first formal calculus to offer full-spectrum dependently typed multi-stage programming with quotation, escape, run, and cross-stage persistence all in one system, making it a foundation for code generators that emit code whose types certify invariants such as fixed vector sizes.","feed_headline":"Multi-stage programming gains dependent types and proven safety","feed_subtitle":"A new calculus, λMD, lets code generators emit code whose types depend on runtime values — and proves it sound.","key_machinery":"The load-bearing mechanism is the stage annotation A decorating every typing judgment, together with the code type ⊲ατ that types quotations. Three rules carry the design: T-Csp embeds a term from stage A into stage Aα; K-Csp silently lifts a well-formed type to a deeper stage, which is how a type such as Vector (%αn) becomes usable inside code; and Q-% equates %αM with M whenever M is already well typed at the deeper stage, so that Vector 5 and Vector (%γ5) count as the same type. Strong normalization is obtained by the ♮-erasure, a translation that erases stages and dependencies down to the simply typed lambda calculus while preserving typing and reduction. The eight mutually recursive judgment forms are what let this argument go through, and they are also the component that must be scrutinized most closely.","core_discovery":"The central claim is that dependently typed multi-stage programming can be made sound by letting every type-theoretic judgment carry a stage annotation. The paper's calculus λMD extends λ⊲% with dependent function types Πx:τ.σ, kinds Πx:τ.K, and code types ⊲ατ, and it handles 'run' as instantiation of a stage abstraction with the empty stage. The key design choice is implicit cross-stage persistence at the type level: a type well-formed at stage A is accepted at stage Aα, so types like Vector (%αn) are usable inside quotations even when the index n is a value from outside. The paper proves that the calculus is well behaved — preservation, strong normalization, confluence for full reduction, and progress for staged reduction — and demonstrates the intended use with a vector-addition code generator whose generated function type mentions the vector length. The paper also claims this is the first formal treatment of full-spectrum dependent types together with quotation, escape, run, and cross-stage persistence.","pith_inferences":["The success of implicit type-level CSP suggests that a practical implementation could erase %α from types during type checking, treating Q-% as a definitional equality rather than an operational step.","The same stage-aware kinding discipline should extend to indexed type families and type operators; the paper already notes that type constructors taking arguments from different stages make term-level CSP necessary, so a matrix type indexed by rows and columns would be a natural test case.","A mechanized proof of the metatheorems would likely need to resolve the example in Section 2.2 where the informal discussion and the K-Csp rule appear to disagree, and such a verification could expose whether the rule set needs a side condition.","Because the paper leaves typechecking algorithms to future work, the next practical step is to design an algorithm that handles implicit type-level CSP and %-erasing equivalence, which the authors identify as the hard parts."],"forward_implications":["Every well-typed λMD term terminates under full reduction, so no infinite reduction sequence can arise from typed code generators.","Full reduction is confluent, which means the result of running a generator does not depend on the order in which redexes are reduced.","The staged, call-by-value semantics is deterministic and every closed well-typed term is either a value or can take exactly one step, so generated code cannot get stuck at run time.","A code generator can return a function whose type mentions a runtime value, and the Q-% equivalence lets that generated code be spliced together with other fragments without a type mismatch."],"supporting_citations":[{"why":"supplies the base multi-stage calculus λ⊲% that λMD extends with dependent types","marker":"[14]"},{"why":"provides the λLF-style dependent type system that the calculus builds on","marker":"[1]"},{"why":"defines environment classifiers and the type-soundness target for MetaOCaml-like multi-stage calculi","marker":"[30]"},{"why":"introduces cross-stage persistence and the MetaML constructs used here","marker":"[31]"},{"why":"describes an earlier dependent-type-plus-staging calculus without run or CSP, the contrast that motivates λMD","marker":"[26]"}],"fun_headline_variants":["Dependent types make multi-stage code generation provably sound","First full-spectrum dependent types for multi-stage programming","λMD: a dependently typed calculus for safe stage manipulation","Multi-stage code generation now dependently typed and proven sound","Dependent types plus cross-stage persistence: proven safe"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The results depend on the eight mutually recursive judgment forms being consistent, and that assumption is not entirely safe: the paper's Section 2.2 says Vector x should not be well-formed at stage α under x:Int@ε, yet its K-Csp rule derives exactly that judgment.","fun_headline_variants_meta":{"raw":{"variants":["Dependent types make multi-stage code generation provably sound","First full-spectrum dependent types for multi-stage programming","λMD: a dependently typed calculus for safe stage manipulation","Multi-stage code generation now dependently typed and proven sound","Dependent types plus cross-stage persistence: proven safe"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000479,"raw_usage":{"total_tokens":2372,"prompt_tokens":946,"completion_tokens":1426,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":562,"completion_tokens_details":{"reasoning_tokens":1346}},"tokens_in":562,"tokens_out":1426,"duration_ms":14974,"temperature":1.0,"reasoning_tokens":1346,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T14:56:34.082261+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Check the derivability of the judgment x:Int@ε ⊢Σ Vector x :: ∗@α: if a formalization of the rules derives it via K-Csp while Section 2.2 claims it is not well-formed, then either the rules or the motivating example must change, and until that is settled the metatheorems cannot be taken as applying to the intended system. A proof assistant can settle this directly by attempting to construct or refute that derivation.","supporting_citations":[{"cited_title":"In: Codish, M., Sumii, E","cited_arxiv_id":null,"evidence_quote":"supplies the base multi-stage calculus λ⊲% that λMD extends with dependent types"},{"cited_title":"In: Pierce, B .C","cited_arxiv_id":null,"evidence_quote":"provides the λLF-style dependent type system that the calculus builds on"},{"cited_title":"In: Pr oc","cited_arxiv_id":null,"evidence_quote":"defines environment classifiers and the type-soundness target for MetaOCaml-like multi-stage calculi"},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"introduces cross-stage persistence and the MetaML constructs used here"},{"cited_title":"In: Proceedings of the Seventh ACM SIGPLAN International Co nference on Func- tional Programming","cited_arxiv_id":null,"evidence_quote":"describes an earlier dependent-type-plus-staging calculus without run or CSP, the contrast that motivates λMD"}],"review_version":1}