Pith. sign in

REVIEW 1 major objections 6 minor 35 references

Circular Proofs as Session-Typed Processes: A Local Validity Condition

T0 review · 1 major / 6 minor · reviewed 2026-08-14 · deepseek-v4-flash

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

Pith's one-line read 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.

desk verdict 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. read the letter →

arxiv 1908.01909 v5 pith:IMD5N7GJ submitted 2019-08-06 cs.LO cs.PL

Farzaneh Derakhshan , Frank Pfenning This is my paper · ORCID
classification cs.LOcs.PL MSC 03F0503B7068Q85
keywords circularproofssessiontypessubsingletonlogicfixedpointslocalvaliditystrongprogresscuteliminationlinear
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

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.

What carries the argument

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.

What would settle it

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).

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

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

  • 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.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

1 major / 6 minor

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.

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 (1)
  1. [Section 11 (Theorem 10)] 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.
minor comments (6)
  1. [Introduction, second paragraph] There is a typo in the name "Fortier and Santoconale"; it should read "Santocanale".
  2. [Definition 5] 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.
  3. [Remark 8] 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.
  4. [Section 13, Example 19] 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.
  5. [Theorem 14] 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.
  6. [Section 14, related work] 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.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: local validity is checked against the external FS guard condition, and the only shared-author citation is a side result that is not load-bearing for the central soundness claim.

full rationale

The derivation chain is not circular. The central soundness claim (Theorem 10) is judged against an external benchmark, Fortier and Santocanale's FS guard condition (Definition 12, from [FS13]), not against the paper's own fitted values. The local validity algorithm (Definition 9, Figure 4) is defined independently via the Call rule, the lexicographic lists of Definitions 4 and 7, and programmer-supplied priorities and partial orders; these inputs are not fitted to FS traces, and the paper explicitly concedes it does not synthesize them (Section 13 and the Implementation paragraph). The only overlapping-author citation, [DP16, Pfe16], is used in Theorem 14 to prove undecidability of a maximal strongly-progressing set; that is a side result about incompleteness and does not justify the validity criterion or the main soundness theorem. One correctness caveat, not a circularity: in Theorem 10 the line 'By Lemma 9 we get X, list( ¯xγ, yδ) (⊂, <Ω′) X, list(¯zα, wβ)' appears to require Lemma 9 to be instantiated at the cycle's starting occurrence and then a transitivity argument along the chain of intermediate calls; Lemma 9 as stated only bounds every call by the original judgment, so the endpoint ordering is under-derived as written. That is a missing proof step, not an equivalence-by-construction or fitted-input prediction, and it does not raise the circularity score.

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

No new physical or logical entities are postulated. Channel generations and the ordering Omega are bookkeeping devices within the proof system, not independent postulates.

free parameters (2)
  • type variable priorities p(t) = user-supplied integer per type variable
    Chosen by the programmer; algorithm soundness holds for any assignment satisfying the signature conditions, but the set of accepted programs depends on it.
  • process variable partial order = family of partial orders on process variables
    User-supplied; used in the combined order in the Call rule. The paper assumes the programmer chooses it based on why strong progress holds (Section 4).
assumptions (4)
  • standard math Standard sequent calculus and linear logic background
    Used throughout; not proved in the paper.
  • domain assumption FS guard condition implies cut elimination (Fortier and Santocanale 2013)
    Used in Section 12 to derive strong progress from local validity.
  • domain assumption Turing machines are encodable as session-typed processes in subsingleton logic with equirecursive types (DeYoung and Pfenning 2016)
    Used in Theorem 14 to prove undecidability.
  • ad hoc to paper The programmer provides a priority assignment and process order satisfying Definition 5
    Needed for the algorithm to be defined; no synthesis method is given.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Circular Proofs as Session-Typed Processes: A Local Validity Condition." pith.science (2026). https://pith.science/paper/IMD5N7GJ

@misc{pith2026190801909,
  author       = {Pith},
  title        = {Pith review of: Circular Proofs as Session-Typed Processes: A Local Validity Condition},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/IMD5N7GJ}},
  note         = {Machine review of arXiv:1908.01909}
}
read the original abstract

Proof theory provides a foundation for studying and reasoning about programming languages, most directly based on the well-known Curry-Howard isomorphism between intuitionistic logic and the typed lambda-calculus. More recently, a correspondence between intuitionistic linear logic and the session-typed pi-calculus has been discovered. In this paper, we establish an extension of the latter correspondence for a fragment of substructural logic with least and greatest fixed points. We describe the computational interpretation of the resulting infinitary proof system as session-typed processes, and provide an effectively decidable local criterion to recognize mutually recursive processes corresponding to valid circular proofs as introduced by Fortier and Santocanale. We show that our algorithm imposes a stricter requirement than Fortier and Santocanale's guard condition, but is local and compositional and therefore more suitable as the basis for a programming language.

Figures

Figures reproduced from arXiv: 1908.01909 by the authors.

Figure 1
Figure 1. Infinitary sequent calculus for subsingleton logi [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Process assignment for subsingleton logic with fix [PITH_FULL_IMAGE:figures/full_fig_p009_2.png] view at source ↗
Figure 3
Figure 3. Infinitary Typing Rules for Processes with Channel [PITH_FULL_IMAGE:figures/full_fig_p027_3.png] view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: Finitary Rules for Local Validity [PITH_FULL_IMAGE:figures/full_fig_p029_4.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

35 extracted references · 35 canonical work pages

  1. [1]

    Least and greatest fixed points in linear logic

    David Baelde. Least and greatest fixed points in linear logic. ACM Transactions on Computational Logic , 13(1):2:1--2:44, 2012

    work page 2012

  2. [2]

    Infinitary proof theory: the multiplicative additive case

    David Baelde, Amina Doumane, and Alexis Saurin. Infinitary proof theory: the multiplicative additive case. In J.-M. Talbot and L. Regnier, editors, 25th Annual Conference on Computer Science Logic (CSL 2016) , pages 42:1--42:17, Marseille, France, August 2016. LIPIcs 62

    work page 2016

  3. [3]

    Intensional type theory with guarded recursive types qua fixed points on universes

    Lars Birkedal and Rasmus Ejlers M gelberg. Intensional type theory with guarded recursive types qua fixed points on universes. In 28th Annual Symposium on Logic in Computer Science (LICS 2013) , pages 213--222, New Orleans, LA, USA, June 2013. IEEE Computer Society

    work page 2013

  4. [4]

    A judgmental analysis of linear logic

    Bor-Yuh Evan Chang, Kaustuv Chaudhuri, and Frank Pfenning. A judgmental analysis of linear logic. Technical Report CMU-CS-03-131R, Carnegie Mellon University, Department of Computer Science, December 2003

    work page 2003

  5. [5]

    Session types as intuitionistic linear propositions

    Lu \' s Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In Proceedings of the 21st International Conference on Concurrency Theory (CONCUR 2010) , pages 222--236, Paris, France, August 2010. Springer LNCS 6269

    work page 2010

  6. [6]

    Linear logic propositions as session types

    Lu \' s Caires, Frank Pfenning, and Bernardo Toninho. Linear logic propositions as session types. Mathematical Structures in Computer Science , 26(3):367--423, 2016. Special Issue on Behavioural Types

    work page 2016

  7. [7]

    Two sides of the same coin: session types and game semantics: a synchronous side and an asynchronous side

    Simon Castellan and Nobuko Yoshida. Two sides of the same coin: session types and game semantics: a synchronous side and an asynchronous side. Proceedings of the ACM on Programming Languages , 3(POPL):1--29, 2019

    work page 2019

  8. [8]

    Cut reduction in linear logic as asynchronous session-typed communication

    Henry DeYoung, Lu \' s Caires, Frank Pfenning, and Bernardo Toninho. Cut reduction in linear logic as asynchronous session-typed communication. In P. C \'e gielski and A. Durand, editors, Proceedings of the 21st Annual Conference on Computer Science Logic (CSL 2012) , pages 228--242, Fontainebleau, France, September 2012. LIPIcs 16

    work page 2012

Show all 35 references
  1. [9]

    Subsingleton

    Ankush Das, Farzaneh Derakhshan, and Frank Pfenning. Subsingleton. https://bitbucket.org/fpfenning/rast/src/master/ss/, June 2019. An implementation of subsingleton logic with ergometric and temporal types

    2019

  2. [10]

    Session-Typed Ordered Logical Specifications

    Henry DeYoung. Session-Typed Ordered Logical Specifications . PhD thesis, Computer Science Department, Carnegie Mellon University, 2020. Forthcoming

    2020

  3. [11]

    On the Infinitary Proof Theory of Logics with Fixed Points

    Amina Doumane. On the Infinitary Proof Theory of Logics with Fixed Points . PhD thesis, Paris Diderot University, France, June 2017

    2017

  4. [12]

    Substructural proofs as automata

    Henry DeYoung and Frank Pfenning. Substructural proofs as automata. In A. Igarashi, editor, 14th Asian Symposium on Programming Languages and Systems , pages 3--22, Hanoi, Vietnam, November 2016. Springer LNCS 10017. Invited talk

    2016

  5. [13]

    Non-wellfounded proof theory for ( K leene+ action) (algebras+ lattices)

    Anupam Das and Damien Pous. Non-wellfounded proof theory for ( K leene+ action) (algebras+ lattices). In Dan R. Ghica and Achim Jung, editors, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018) . LIPIcs 119, 2018

    2018

  6. [14]

    Cuts for circular proofs: Semantics and cut-elimination

    J \'e r \^o me Fortier and Luigi Santocanale. Cuts for circular proofs: Semantics and cut-elimination. In Simona Ronchi Della Rocca, editor, 22nd Annual Conference on Computer Science Logic (CSL 2013) , pages 248--262, Torino, Italy, September 2013. LIPIcs 23

    2013

  7. [15]

    Linear logic and lazy computation

    Jean-Yves Girard and Yves Lafont. Linear logic and lazy computation. In H. Ehrig, R. Kowalski, G. Levi, and U. Montanari, editors, Proceedings of the International Joint Conference on Theory and Practice of Software Development , volume 2, pages 52--66, Pisa, Italy, March 1987...

    1987

  8. [16]

    Guarded Recursive Type Theory

    Hans Brugge Grathwohl. Guarded Recursive Type Theory . PhD thesis, Department of Computer Science, Aarhus University, Denmark, September 2016

    2016

  9. [17]

    Polarized Substructural Session Types

    Dennis Griffith. Polarized Substructural Session Types . PhD thesis, University of Illinois at Urbana-Champaign, April 2016

    2016

  10. [18]

    Gay and Vasco T

    Simon J. Gay and Vasco T. Vasconcelos. Linear type theory for asynchronous session types. Journal of Functional Programming , 20(1):19--50, January 2010

    2010

  11. [19]

    Types for dyadic interaction

    Kohei Honda. Types for dyadic interaction. In 4th International Conference on Concurrency Theory , CONCUR'93, pages 509--523. Springer LNCS 715, 1993

    1993

  12. [20]

    W. A. Howard. The formulae-as-types notion of construction. Unpublished note. An annotated version appeared in: To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, 479--490, Academic Press (1980), 1969

    1980

  13. [21]

    Vasconcelos, and Makoto Kubo

    Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In 7th European Symposium on Programming Languages and Systems (ESOP 1998) , pages 122--138. Springer LNCS 1381, 1998

    1998

  14. [22]

    The size-change principle for mixed inductive and coinductive types

    Pierre Hyvernat. The size-change principle for mixed inductive and coinductive types. arXiv preprint arXiv:1901.07820 , 2019

    1901 arXiv

  15. [23]

    Free lattices, communication and money games

    Andr \' e Joyal. Free lattices, communication and money games. In Logic and Scientific Methods: Volume One of the Tenth International Congress of Logic, Methodology and Philosophy of Science, Florence, August 1995 , volume 259, page 29. Springer Science & Business Media, 1996

    1995

  16. [24]

    Around classical and intuitionistic linear logic

    Olivier Laurent. Around classical and intuitionistic linear logic. In A. Dawar and E. Gr \"a del, editors, Proceedings of the 33rd Annual Symposium on Logic in Computer Science (LICS 2018) , pages 629--638, Oxford, UK, July 2018. ACM

    2018

  17. [25]

    Garrett Morris

    Sam Lindley and J. Garrett Morris. Talking bananas: Structural recursion for session types. In J. Garrigue, G. Keller, and E. Sumii, editors, Proceedings of the 21st International Conference on Functional Programming , pages 434--447, Nara, Japan, September 2016. ACM Press

    2016

  18. [26]

    Local validity for circular proofs in linear logic with fixed points

    R \'e mi Nollet, Alexis Saurin, and Christine Tasson. Local validity for circular proofs in linear logic with fixed points. In D. Ghica and A. Jung, editors, 27th Annual Conference on Computer Science Logic (CSL 2018) , pages 35:1--35:23. LIPIcs 119, 2018

    2018

  19. [27]

    Substructural logics

    Frank Pfenning. Substructural logics. Lecture notes for course given at Carnegie Mellon University, Fall 2016, December 2016

    2016

  20. [28]

    Local type inference

    Benjamin C Pierce and David N Turner. Local type inference. ACM Transactions on Programming Languages and Systems (TOPLAS) , 22(1):1--44, 2000

    2000

  21. [29]

    Reuben N. S. Rowe and James Brotherston. Automatic cyclic termination proofs for recursive procedures in separation logic. In Y. Bertot and V. Vafeiadis, editors, Proceedings of the 6th Conference on Certified Programs and Proofs (CPP 2017) , pages 53--65, Paris, France, Janua...

    2017

  22. [30]

    A calculus of circular proofs and its categorical semantics

    Luigi Santocanale. A calculus of circular proofs and its categorical semantics. In M. Nielsen and U. Engberg, editors, 5th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2002 , pages 357--371, Grenoble, France, April 2002. Sprin...

    2002

  23. [31]

    Free -lattices

    Luigi Santocanale. Free -lattices. Journal of Pure and Applied Algebra , 168(2-3):227--264, 2002

    2002

  24. [32]

    From parity games to circular proofs

    Luigi Santocanale. From parity games to circular proofs. Electronic Notes in Theoretical Computer Science , 65(1):305--316, 2002

    2002

  25. [33]

    -bicomplete categories and parity games

    Luigi Santocanale. -bicomplete categories and parity games. Informatique Th \'e orique et Applications , 36(2):195--227, 2002

    2002

  26. [34]

    Higher-order processes, functions, and sessions: A monadic integration

    Bernardo Toninho, Lu \' s Caires, and Frank Pfenning. Higher-order processes, functions, and sessions: A monadic integration. In M.Felleisen and P.Gardner, editors, Proceedings of the European Symposium on Programming (ESOP'13) , pages 350--369, Rome, Italy, March 2013. Spring...

    2013

  27. [35]

    Propositions as sessions

    Philip Wadler. Propositions as sessions. In Proceedings of the 17th International Conference on Functional Programming , ICFP 2012, pages 273--286, Copenhagen, Denmark, September 2012. ACM Press

    2012

Pith tools

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