{"id":"464b8f01-9c61-48e0-9f3f-9b0709ce342b","arxiv_id":"1908.01909","paper_version":5,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":2,"one_line_summary":"A local, compositional, decidable validity condition on session-typed recursive processes that implies Fortier and Santocanale's guard condition and strong progress.","lead":"This paper gives a way to check, piece by piece, whether recursively defined communicating processes correspond to valid circular proofs in a logic with fixed points. The check is fast and guarantees that accepted processes eventually try to communicate with the outside world.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 10's proof does not derive the required endpoint ordering for a cycle from Lemma 9; the per-call local validity check needs to be instantiated at the cycle's start, and this step is missing.","rationale":"The reader identified the reliance on programmer-supplied priorities and process-variable orders as the weakest assumption. That is a practical incompleteness explicitly acknowledged by the authors (Section 13, implementation discussion). The more load-bearing concern is a gap in the proof of the central soundness theorem (Theorem 10). The proof as written does not follow from Lemma 9, because Lemma 9 only relates calls to the original formal head, not to an earlier occurrence in a cycle. Without an additional instantiation argument, the theorem's conclusion that every cycle is a left mu-trace or right nu-trace is not derived. This is a correctness gap in the central claim, not merely a practical limitation. Since the gap appears repairable and the theorem itself may well be true, a conditional accept with a request to repair the proof is appropriate. The concrete formalization test would settle whether the missing step is genuinely needed or whether a hidden assumption in Lemma 9 already suffices.","tokens_in":43600,"tokens_out":26500,"duration_ms":257018,"concrete_test":"Formalize Lemma 9 and Theorem 10 in a proof assistant (Coq/Lean) and attempt to complete the proof of Theorem 10. If the proof cannot be completed without adding the instantiation argument explicitly, attempt to construct a program where two recursive calls to the same process variable each satisfy the local Call rule against the formal head channels but the path connecting the two calls has no strict decrease in list(x,y). Such a program would satisfy local validity yet violate the FS guard condition, disproving Theorem 10.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The proof of Theorem 10 (Section 11) considers a cycle between two occurrences of Def X, with channels (x^gamma, y^delta) at the top and (z^alpha, w^beta) at the bottom, and claims: 'By Lemma 9 we get X, list(x^gamma,y^delta) (⊂,<) X, list(z^alpha,w^beta).' However, Lemma 9's 'Moreover' clause states only that every call in the infinite derivation is less than the original formal channels (x^alpha, y^beta) of the judgment being checked. Applying it to the top occurrence gives X,list(x^gamma,y^delta) < X,list(x^alpha,y^beta); applying it to the bottom occurrence gives X,list(z^alpha,w^beta) < X,list(x^alpha,y^beta). These two inequalities do not imply the needed order between the top and bottom of the cycle. The missing argument is that the finite local-validity derivation of X's definition, when instantiated at the actual channels of the top occurrence, gives the Call rule check for the recursive call (the cycle's bottom) directly as list(z^alpha,w^beta) < list(x^gamma,y^delta). The proof as written skips this instantiation step, so the central soundness claim is not established as stated.","agreement_with_reader":"disagree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper extends the Curry-Howard correspondence between intuitionistic linear logic and session-typed processes to subsingleton logic with least and greatest fixed points. The central technical contribution is a finitary, compositional validity condition for mutually recursive session-typed processes, called local validity, which is checked by the rule system in Figure 4. The authors prove that every locally valid program satisfies the Fortier--Santocanale guard condition (Theorem 10), and therefore inherits cut elimination and a strong progress property (Theorems 12--13). They also show that the condition is stricter than the FS guard condition, that no effective procedure can recognize a maximal set of strongly progressing programs closed under composition (Theorem 14), and that their validity check runs in time linear in the total input (Remark 8). The paper is illustrated with many worked examples and includes an implementation reference.","tokens_in":43871,"tokens_out":11806,"duration_ms":116109,"significance":"If the main soundness theorem is correct, this is a valuable contribution: it gives a local, syntax-directed, and compositional criterion for recognizing valid circular proofs in a session-typed setting, with a linear-time algorithm and a public implementation. The paper is careful to compare against the external benchmark of Fortier--Santocanale rather than fitting parameters to a target, and it explicitly discloses the main practical limitation, namely that type-variable priorities and process-variable orders are programmer-supplied (Definition 5, Example 19, Section 13). The central gap I identify below concerns the proof of Theorem 10, not the statement of the algorithm or its examples; the gap is local and appears repairable with an instantiation argument using Proposition 4, but as written the proof of the main soundness claim is incomplete.","major_comments":[{"comment":"The proof of Theorem 10 contains a load-bearing gap. The proof considers a cycle between two occurrences of Def X and claims: \"By Lemma 9 we get X, list(¯x^γ, y^δ) (⊂,<Ω′) X, list(¯z^α, w^β).\" Lemma 9's \"Moreover\" clause, however, compares every call in the produced infinite derivation to the fixed original channels and process variable of the judgment that was checked; it does not compare one call to another. Applying Lemma 9 to the top occurrence gives a comparison with the original formal channels, and applying it to the bottom occurrence gives another comparison with the same right-hand side; the two inequalities do not imply the needed ordering between the top and bottom occurrences of the cycle. The missing step is to instantiate the finite local-validity derivation of X's definition at the actual channels of the top occurrence (using Proposition 4, whose hypotheses are satisfied because the relevant future generations are fresh) and then to apply the Call rule at the recursive call that forms the cycle's bottom; this directly yields list(¯z^α, w^β) < list(¯x^γ, y^δ) or the analogous process-variable comparison. Until this argument is supplied, the proof of the paper's central soundness claim is incomplete.","section":"Section 11 (Theorem 10)"}],"minor_comments":[{"comment":"There is a typo in the name \"Fortier and Santoconale\"; it should read \"Santocanale\".","section":"Introduction, second paragraph"},{"comment":"The notation \"X /simequali Y\" is corrupted in the text; it should be typeset as a proper equivalence symbol, and the phrase \"for some (unique) i\" in part (c) would benefit from an explicit explanation of why uniqueness follows from the disjointness of the family of partial orders.","section":"Definition 5"},{"comment":"The claim that type-checking itself is bounded below by O(m + s^2) is stated without justification or reference; either provide a proof sketch or soften the comparison, since the lower bound is not central to the complexity claim about validity checking.","section":"Remark 8"},{"comment":"The sentence \"This implies that the number of messages w0←Empty←· may receive along channel w0 is strictly less than the number of messages received by any process along channel yβ\" is vague; specifying the particular instance of Empty along yβ would make the comparison precise.","section":"Section 13, Example 19"},{"comment":"The proof relies on the assertion that the DeYoung--Pfenning encoding of Turing machines, which uses equirecursive types, is \"easily embedded\" into the isorecursive setting; since Theorem 14 depends on this embedding, please give a reference or a brief construction.","section":"Theorem 14"},{"comment":"The sentence \"their language cannot be reduced to circular proofs\" (referring to Hyvernat's work) needs a brief gloss or citation, as the reader is left to infer the reason.","section":"Section 14, related work"}],"recommendation":"major_revision","confidential_remarks":"The gap in Theorem 10 is genuine but local; the intended repair via Proposition 4 and the Call rule is natural and likely within scope. I recommend major revision rather than rejection, and I expect the paper to become acceptable once the proof is repaired. The paper fits the journal's scope well."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The paper gives a local, compositional validity check for recursive session-typed processes over mixed inductive/coinductive types. That result is new and, as far as I can tell, correct. The algorithm is decidable and linear-time, strictly implies Fortier and Santocanale's guard condition, and gives strong progress for accepted programs. The authors are honest about incompleteness (Example 19) and undecidability of any maximal closed class (Theorem 14), and they cite the relevant prior work without padding. The implementation is referenced and publicly available.\n\nThe one real soft spot is in the proof of Theorem 10. The stress-test note is right: Lemma 9's 'Moreover' clause compares every call in the infinite derivation to the original judgment's channels, not to another occurrence in the same cycle. Two calls can both be below the original without being ordered with respect to each other. The proof says 'By Lemma 9 we get X,list(x^γ,y^δ) < X,list(z^α,w^β)' without justification. The intended fix is to apply Proposition 4 (instantiation) to the finitary derivation of X's body at the lower Def occurrence—the start of the cycle—and then apply Lemma 9 to that sub-derivation. That gives the needed comparison. It's a routine two-line repair, but as written the soundness proof has a gap, and it should be flagged before publication.\n\nThe rest of the proof structure holds up. The lexicographic argument after the list inequality is sound: the first strict decrease in the flattened list has to be at a receive component, so the case split into left µ-trace or right ν-trace is exhaustive. Lemmas 6 and 7 in the appendix are detailed enough to follow.\n\nOverall: this is a genuine contribution, not a desk reject. The main theorem is load-bearing, so the gap in its proof matters, but it is clearly repairable. I would send it to a good referee and expect acceptance after a minor revision. For a reading group in session types or circular proof theory, it's worth an hour.","headline":"A genuine, novel local validity criterion for recursive session-typed processes, worth serious review; the proof of Theorem 10 has a repairable gap that needs to be written out.","tokens_in":44398,"tokens_out":18427,"would_cite":true,"duration_ms":173071,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03F05","03B70","68Q85"],"pacs":[],"model":"deepseek-v4-flash","headline":"Locally valid programs—those that pass the generation-comparison check at every recursive call—satisfy the guard condition for circular proofs and therefore never diverge internally.","keywords":["circular proofs","session types","subsingleton logic","fixed points","local validity","strong progress","cut elimination","linear logic"],"falsifier":"Produce a process definition accepted by the Call rule whose infinite derivation contains a cycle that is neither a left µ-trace nor a right ν-trace: along the cycle, the highest-priority fixed-point rule on the left is not a positive unfolding (µL) and the highest-priority fixed-point rule on the right is not a negative unfolding (νR).","tokens_in":43384,"feed_emoji":"🔄","tokens_out":7777,"duration_ms":73876,"temperature":0.7,"pith_summary":"The paper aims to bring recursion into the proofs-as-processes reading of linear logic without losing logical soundness, by isolating a decidable, local condition under which mutually recursive session-typed processes correspond to valid circular proofs. The central claim is that a program is safe exactly in the sense of the paper's local validity check: every process definition, checked independently, must show a lexicographic decrease in a list of channel generations at every recursive call, using priorities of fixed-point types and a partial order on process variables. If a program passes this check, the paper proves it satisfies the earlier guard condition for circular proofs, hence cut elimination holds; as a computational corollary, every valid configuration either terminates empty or attempts to communicate on an external channel after finitely many steps. Because the condition is local and linear-time, the paper argues it is a more practical basis for a programming language than the global guard condition, while remaining strictly more restrictive.","feed_headline":"Recursive session processes pass a local check or loop forever","feed_subtitle":"Each process definition is verified in isolation, guaranteeing cut elimination and strong progress in linear time.","key_machinery":"The load-bearing object is the finitary typing judgment with channel generations, written ⟨ū^γ, X, v^δ⟩; ẑ^α : ω ⊢_{Ω,⊂} P :: (w^β : C). Here each channel carries a generation superscript, and Ω records how generations compare for each fixed-point priority: receiving an unfolding message for priority i registers an inequality like $x^{{α+1}}$_i < x^α_i, while sending one registers equality with lower-priority components. The Call rule replaces the Def rule: at a call to Y with current channels (ẑ^α, w^β), it requires Y, list(ẑ^α, w^β) to be strictly smaller, in the lexicographic order (⊂,<) that also places the process variable order, than the saved X, list(ū^γ, v^δ). Accepting every call in every definition is local validity. This mechanism carries the argument because a call that is accepted necessarily produces an index i where the left generation decreases for a positive priority or the right generation decreases for a negative priority, which is exactly the trace condition the guard condition demands.","core_discovery":"The paper's central claim is Theorem 10: locally valid programs satisfy the guard condition for circular proofs. Concretely, if every process definition passes the Call rule of Figure 4, then every cycle in the infinite derivation is either a left µ-trace or a right ν-trace; by the referenced cut-elimination theorem, such proofs admit cut elimination. The proof works by reading the finitary local derivation as an infinite derivation in which each accepted recursive call forces a strict decrease in the combined order (⊂,<) on the list of channel generations. The paper then draws the computational consequence (Theorem 13): a configuration of locally valid processes cannot run forever in internal communication; after finitely many steps it is empty or communicating with the outside. It also notes that no effective procedure can recognize a maximal compositional set of programs satisfying that strong progress property, since termination of Turing machines can be encoded.","pith_inferences":["If the programmer-supplied priorities and process orders are chosen badly, the algorithm may reject reactive programs; a practical language would therefore need constraint synthesis or interactive annotation, an issue the paper leaves open.","The same generation-comparison technology could serve as a termination measure for other cyclic proof systems, since it only needs a well-founded order on channels indexed by fixed-point priorities.","One testable extension is to integrate the local check with a size-change principle for mixed inductive/coinductive data, potentially yielding a more complete but still local criterion than the one presented here.","The visibility function c(A) suggests that the check is modular across type definitions; a compiler could cache visibility sets to make the linear-time bound practical."],"forward_implications":["Programs accepted by the local check satisfy strong progress: no infinite internal communication without an eventual external send or receive.","Validity composes: putting two locally valid programs in sequence over the same signature yields a locally valid program, so strong progress is preserved under cut.","The validity check runs in time O(n(m+s)), linear in the program plus signature, in contrast to the PSPACE bound known for the global guard condition.","The underlying circular proofs have the cut-elimination property, connecting the programming-language mechanism to logical consistency.","No decidable criterion can be complete for the maximal set of strong-progress programs closed under composition, so local validity is a decidable sufficient condition rather than an exact characterization."],"supporting_citations":[{"why":"Defines the guard condition on circular proofs and proves cut elimination for guarded derivations; this is the condition Theorem 10 shows local validity implies.","marker":"[FS13]"},{"why":"Establishes the correspondence between intuitionistic linear logic and session-typed processes that the paper extends with least and greatest fixed points.","marker":"[CPT16]"},{"why":"Gives the encoding of Turing machines as session-typed processes in subsingleton logic, used to prove undecidability of any complete strong-progress criterion.","marker":"[DP16]"},{"why":"Shows the guard condition for circular proofs in MALL with fixed points is PSPACE-decidable, providing the complexity baseline the linear-time local check is compared against.","marker":"[Dou17]"},{"why":"Provides an earlier local polynomial-time validity algorithm for a stricter version of Baelde's condition, which the paper contrasts with its own local condition.","marker":"[NST18]"},{"why":"Supplies the notion of local type inference that the paper adopts when saying its validity check is local.","marker":"[PT00]"}],"fun_headline_variants":["Local validity check guarantees no infinite loops","Compositional check replaces global guard for circular proofs","Decidable local criterion for circular proof validity","Local check for session processes proves termination","One local rule eliminates runaway session loops"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The algorithm takes as input a priority for every type variable and a partial order on process variables; the paper does not explain how a programmer should choose these annotations, and a program may satisfy strong progress while no such annotation makes it locally valid.","fun_headline_variants_meta":{"raw":{"variants":["Local validity check guarantees no infinite loops","Compositional check replaces global guard for circular proofs","Decidable local criterion for circular proof validity","Local check for session processes proves termination","One local rule eliminates runaway session loops"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000703,"raw_usage":{"total_tokens":3132,"prompt_tokens":863,"completion_tokens":2269,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":479,"completion_tokens_details":{"reasoning_tokens":2204}},"tokens_in":479,"tokens_out":2269,"duration_ms":16142,"temperature":1.0,"reasoning_tokens":2204,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T14:59:45.547785+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Produce a process definition accepted by the Call rule whose infinite derivation contains a cycle that is neither a left µ-trace nor a right ν-trace: along the cycle, the highest-priority fixed-point rule on the left is not a positive unfolding (µL) and the highest-priority fixed-point rule on the right is not a negative unfolding (νR).","supporting_citations":[],"review_version":1}