Pith. sign in

REVIEW 3 major objections 6 minor 42 references

A Type-and-Effect System for Temporal Dependency Analysis of Render-based Reactive Programs

T0 review · 3 major / 6 minor · reviewed 2026-07-30 · grok-4.5

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

Pith's one-line read Willow turns React-style render timing into checkable effects so cascades, loops, and stale handlers show up before runtime.

desk verdict Solid PL core calculus with a real effect algebra for React-style timing; the multi-render graph story is useful but less formally pinned than the one-step preservation. read the letter →

arxiv 2607.27074 v1 pith:SIY7Z5MV submitted 2026-07-29 cs.PL cs.SE

June Wunder , Ankush Das , Marco Gaboardi This is my paper · ORCID
classification cs.PLcs.SE
keywords reactiveprogrammingtype-and-effectsystemsReacttemporaldependencygraphsrendersemanticseventhandlerlifecyclegradedmodalitiesstaticanalysis
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

Interactive UI frameworks let you declare how the screen depends on state, but they hide when updates fire, when handlers bind or unbind, and how one change can cascade into many renders. Willow is a small React-inspired calculus that makes that timing first-class: a two-phase semantics (render, then housekeeping) paired with a type-and-effect system. Effects record delayed state changes with a graded “next” modality counted in renders, milliseconds, or network trips, and a family of modalities for registering, firing, canceling, and removing event handlers. Those effects form a temporal dependency graph, so ordinary graph walks can flag long render cascades, inter-render loops, expensive high-frequency handlers, missing cleanups, and first-paint cost. The authors prove that well-typed programs preserve their effect annotations under an instrumented semantics, ship a prototype with automatic inference, and show it surfacing stuck loading states, request races, and update loops in realistic patterns like debounce and signup forms.

What carries the argument

The temporal dependency graph built from Willow effects—especially the graded next modality ○ᴺᵘ and the handler lifecycle modalities 2/3/⊘/7—carries the argument: effects over-approximate when state may change and when listeners are bound or torn down, and graph expansion recovers full multi-render consequences including loops.

What would settle it

Port the checker to a non-toy React hooks codebase that uses dynamic component mount/unmount and concurrent features; if the inferred graphs miss known render loops or stale-listener bugs that appear in the real runtime, or flood false positives on correct code, the transfer claim fails.

Watch

Extended reading notes

Core claim

Time-aware typing of render-based reactive programs is practical: if you treat renders as the unit of time and track state updates plus the full event-handler lifecycle as graded effects, the resulting temporal dependency graph lets standard graph algorithms statically catch the timing bugs that framework runtimes usually bury, and those effects are preserved by a time-aware operational semantics.

Load-bearing premise

The simplified two-phase model (no mount/unmount, no concurrent scheduler lanes, only static event labels) is close enough to real React that the static warnings still mean something in production apps.

Editorial extensions

If this is right

  • Debounce, form validation, and API-check patterns can carry types that visibly place network work behind timers and show race or stuck-status bugs at compile time.
  • Inter-render feedback loops and missing handler cleanups become graph properties rather than runtime surprises.
  • First-render cost and high-frequency expensive handlers can be warned about from the same effect graph without running the app.
  • Library authors can expose temporal contracts (e.g. “this fetch is debounced”) that compose through parent components via effect polymorphism.

Reading between the lines

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

  • Extending the system with dependent vertex structures for dynamic mount/unmount, as the paper itself flags, is the main bridge from the core calculus to production React tooling.
  • The same graded-next and handler-lifecycle effects could likely annotate other virtual-DOM or signal-based UI runtimes, not only React-shaped ones.
  • Once effects are in the type, CI could gate merges on “no new inter-render loops” or “no unbound high-frequency handlers” the way linters gate complexity today.
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.

Referee Report

3 major / 6 minor

Summary. Willow is a React-inspired core calculus with a two-phase (render/housekeeping) operational semantics and a type-and-effect system that tracks state updates, event-handler lifecycle (bind/once/cancel/remove), and delays via a graded next modality ○ over host units (renders, ms, network). Effects inhabit an algebra with sequencing, branching, and event-guarded modalities; cascading effects live in an environment Δ and are expanded post-check into temporal dependency graphs on which the authors run standard graph algorithms for inter-render loops, render cascades, stale listeners, high-frequency handlers, and first-render cost. The paper proves preservation of effects w.r.t. an instrumented trace semantics (Theorem 6.1 / Appendix F), implements Hindley–Milner-style effect inference in Haskell, and evaluates on debounce, MovingDot, mutual recursion, and a signup-form case study that surfaces a stuck loading state, a request race, and a deliberate retry loop.

Significance. If the results hold at the stated scope, the work is a solid contribution to typed reactive programming: it makes render-relative and mixed-unit timing first-class in an effect system, unifies handler registration/teardown with state cascades, and shows that the resulting graphs support useful static warnings. Strengths include a detailed preservation development (configurations, declarations, expressions, queue typing, causes, subeffecting), a working inference prototype that checks every paper example, and a concrete case study that finds real timing bugs. The fidelity gap to full React (no mount/unmount, no concurrent lanes, static event labels) is acknowledged; within the simplified model the approach is a credible foundation for further work rather than an immediate drop-in React analyzer.

major comments (3)
  1. [§5.4, Theorem 6.1 / Appendix F] Abstract, Contributions, and §5.4 claim that inferred effects form temporal dependency graphs on which standard algorithms “statically detect” render cascades and inter-render loops. Theorem 6.1 / F.1 only guarantees that a change in X produces a sub-effect of the Δ cascade in the next housekeeping queue (justify-on). The multi-render full-effect expansion (recursive unfolding of ○, 2/3, ∗/+, loop[·] markers; §5 “Immediate, cascading, and full effects”) is never stated as a corollary relating operational multi-render traces to paths/cycles in that graph, including across mixed units (r vs ms vs n) and + branches. Either prove a soundness lemma for the expansion (over-approximation of multi-step traces) or clearly demote cascade/loop detection to a post-hoc heuristic justified only up to one cascade step plus informal graph reading.
  2. [Abstract; Conclusion; §4; ty subcomp decl] The central “practical foundation for … reactive programs” claim (Abstract; Conclusion) rests on a deliberately simplified semantics: immutable render phase, single event queue, no component mount/unmount, no React priority lanes or concurrent features, and only statically known event-label tuples (Conclusion; Related Work vs React-tRace). Subcomponent typing is α-renaming plus Δ_A ⊆ Δ (ty subcomp decl). These restrictions are load-bearing for transfer to real React; the paper flags mount/unmount as future dependent vertex structure work but still markets the analyses as catching defects “missed by compiler transformations and other current tools.” Scope the evaluation and claims explicitly to Willow’s model, and qualify every React-transfer sentence accordingly.
  3. [§7] Evaluation (§7) is a prototype inference run on hand-written patterns (debounce, MovingDot, mutual recursion, one signup form). There is no corpus study, no comparison against existing React linters/compilers, no false-positive/negative accounting, and no measurement of annotation burden beyond “minimal.” The signup-form findings are illuminating but anecdotal. For the claim that the system “statically finds and draws attention to timing bugs,” add at least a small structured case suite with expected warnings, or soften the empirical language to “feasibility demonstration.”
minor comments (6)
  1. [§2–§5] Notation for modalities is inconsistent across the text (○1𝑟 vs ○^{1r}, 2 vs □-like square, 7 vs remove glyph). Pick one rendering and stick to it in body, figures, and appendix.
  2. [Fig. 1; Fig. 7; Fig. 13] Figure 1 syntax uses if 𝑥 then … (variable scrutinee) while expression typing/semantics allow general 𝑒1; align syntax and rules.
  3. [§5] df (dataflow function) is left as a parameter with “simplest instantiation = free variables.” State how the prototype instantiates df and whether imprecise df affects soundness of causes or only precision of cascades.
  4. [§8] Related work on FRP/modal FRP (Fran, Simply RaTT, ultrametric FRP) and graded monads is appropriate; a short explicit contrast table (what Willow tracks that React-tRace/λreact do not, and vice versa) would help readers.
  5. [throughout] Typos and spacing: “Reactiveprogrammingframeworks”, “timing as-sumptionsburied”, “aprototypetype-and-effect”, “theseeffectscanbecomposed” suggest PDF generation issues; clean the camera-ready text.
  6. [§6; Appendix F] Appendix F is long and useful; cross-reference key lemmas (Flush Queue Preservation, Listen typing inversion, expression listener-safety) from the main Theorem 6.1 statement so readers can navigate.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: standard PL metatheory (syntax, semantics, effects, preservation) with post-hoc graph analyses defined on the effect algebra, not fitted or self-justified predictions.

full rationale

Willow’s derivation chain is the ordinary formal-methods pattern: a core calculus with two-phase render/housekeeping semantics, a type-and-effect system whose effects are introduced by typing rules for setters and event primitives, a preservation theorem (Thm 6.1 / F.1) proved against an instrumented semantics with traces, and post-typecheck analyses that treat inferred effects as a temporal dependency graph. Nothing in that chain is equivalent to its inputs by construction. Effects are not fitted to runtime traces or empirical timing data; cascade and full-effect expansion are defined operations on Δ and the effect grammar (○, ∗, +, 2/3, etc.), and loop/cascade/stale-listener checks are standard graph walks over that structure. Self-citations (Das et al. temporal session types; Rinaldi et al. graph types with overlapping authors) appear only as related-work inspiration for modalities and future mount/unmount extensions, not as load-bearing unproven lemmas inside the preservation argument, which is developed self-contained in the appendix. Gaps the skeptic notes—that multi-render full-effect soundness is not a stated corollary of Thm 6.1, and that the simplified semantics omits mount/unmount—are fidelity or completeness concerns, not circular reductions of claim to input. Score 0 with empty steps is the correct outcome.

Assumptions & free parameters 0 free parameters · 5 assumptions · 3 invented entities

Load-bearing content is definitional (the Willow calculus and effect algebra) plus standard PL metatheory. Domain assumptions encode a simplified React execution model. No numeric free parameters. Invented entities are the calculus constructs themselves, which is normal for a core-calculus paper; independent evidence is the prototype and the worked bug-finding examples rather than external physical measurement.

assumptions (5)
  • domain assumption Render-based execution is adequately modeled by alternating immutable render phases and housekeeping flushes of a single ordered event queue, with external events admitted only between renders.
    Stated throughout §4; deliberately simplifies React’s concurrent lanes, microtasks, and priority scheduling.
  • domain assumption Event labels ℓ⟨v⟩ carry only statically known discriminant tuples; dynamic ids cannot enter the effect layer.
    §2–3; required so effects remain a static algebra.
  • domain assumption A dataflow function df soundly over-approximates expression dependencies (default: free variables).
    §5; used to populate Δ cascading entries for let-bound variables.
  • standard math Standard type-and-effect and operational-semantics metatheory (preservation via instrumented traces, subeffecting as a preorder, graded-monoid laws for ○).
    Used throughout §5–6 and Appendix F.
  • domain assumption External scheduler ℰ is well-behaved: payloads inhabit Σ_E and the scheduler may be treated as an opaque source of typed firings.
    §6 / Appendix D; no timing guarantees claimed across units.
invented entities (3)
  • Willow core calculus (components, on-blocks, bind/once/cancel/remove) independent evidence
    purpose: Minimal React-inspired language on which timing can be made explicit
    Defined in §3; standard core-calculus move, not an extra physical postulate.
  • Graded effect algebra with ○^{N_u}, 2_e, 3_e, ⊘_e, 7_e, ∗, + independent evidence
    purpose: Statically record when state changes and listener lifecycle actions may occur
    §5; the central technical invention; evidence is the preservation proof and prototype inference.
  • Temporal dependency graph extracted from Δ and effects independent evidence
    purpose: Enable off-the-shelf graph algorithms for cascades, loops, stale handlers, first-render cost
    §5.4; derived view of the effect algebra rather than a new ontological claim.

how reviews work

0 comments
Cite this review

Pith. "Pith review of A Type-and-Effect System for Temporal Dependency Analysis of Render-based Reactive Programs." pith.science (2026). https://pith.science/paper/SIY7Z5MV

@misc{pith2026260727074,
  author       = {Pith},
  title        = {Pith review of: A Type-and-Effect System for Temporal Dependency Analysis of Render-based Reactive Programs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/SIY7Z5MV}},
  note         = {Machine review of arXiv:2607.27074}
}
read the original abstract

Reactive programming frameworks such as React allow developers to build interactive applications by declaratively specifying how outputs depend on changing inputs. Although this model makes it easy to reason about what an application computes, the temporal behavior of reactive programs remains difficult to understand and verify. Applications implicitly rely on timing assumptions buried in framework runtimes, leading to subtle bugs such as stale reads, transient inconsistencies, order-dependent behavior, and unintended feedback cycles. To address these challenges, this paper presents Willow, a core calculus for reactive programming inspired by React. Willow gives a time-aware operational semantics that models computation in terms of renders, the fundamental evaluation step in which components produce user interface descriptions, and pairs it with a novel type-and-effect system that statically tracks timing behavior as effects. A "next" modality expresses delays measured not only in renders but in any unit the host environment exposes--renders, network requests, or milliseconds. A family of modalities tracks the lifecycle of event handlers: when they are registered, when they fire, when pending events are canceled and when handlers are removed. A key insight is that the resulting effects form a temporal dependency graph, letting standard graph algorithms statically detect render cascades and inter-render loops that cause non-termination or performance degradation. We formalize Willow and prove preservation of the effect system with respect to the time-aware semantics. We also implement a prototype checker with automatic effect inference and evaluate it on representative reactive patterns such as debouncing, form inputs, and API-driven updates. Our results demonstrate that time-aware typing provides a practical foundation for reasoning about the temporal correctness of reactive programs.

Figures

Figures reproduced from arXiv: 2607.27074 by the authors.

Figure 1
Figure 1. Syntax of Willow Programs The effect of changing x is ○ 1𝑟 @𝑦; and vice versa, the effect for changing y is ○ 1𝑟 @𝑥. From the graph, we can infer that the full effect of modifying x is an infinite chain of modifications of x and y. Willow can auto-detect this kind of error and warn the programmer at compile time. 3 Formal Syntax Willow’s syntax is inspired by React with a few simplifications. Like React, Willow prog… view at source ↗
Figure 2
Figure 2. Selected component-level semantics rules [PITH_FULL_IMAGE:figures/full_fig_p012_2.png] view at source ↗
Figure 3
Figure 3. Re-render declaration-level semantics rules. [PITH_FULL_IMAGE:figures/full_fig_p013_3.png] view at source ↗
Figures from the paper (34 more)
Figure 4
Figure 4. Figure 4: Selected expression-level semantics rules. [PITH_FULL_IMAGE:figures/full_fig_p014_4.png]
Figure 5
Figure 5. Figure 5: Grammar of Willow Types and Effects corresponds to an event in the environment Willow is embedded in. On the web this can be a keypress, a mouse movement, a network request. The primary vehicle of timing analysis is the temporal next modality ○ 𝑁 whose superscript 𝑁 co…
Figure 6
Figure 6. Figure 6: Declaration-level typing rules. 5.1 Declaration-Level Typing Rules The declaration typing derivation is Σ ; Δ ; Γ1 ⊢ 𝑝 ⇒ Γ2 , where Σ is the program signature, which maps each component name to its code, effect environment, and typing environment. Δ is the current comp…
Figure 7
Figure 7. Figure 7: Selected expression-level typing rules, including the four event primitives. [PITH_FULL_IMAGE:figures/full_fig_p018_7.png]
Figure 8
Figure 8. Figure 8: Syntax of Willow Programs (reproduced from Figure [PITH_FULL_IMAGE:figures/full_fig_p028_8.png]
Figure 9
Figure 9. Figure 9: Grammar of Willow Types and Effects (reproduced from Figure [PITH_FULL_IMAGE:figures/full_fig_p028_9.png]
Figure 10
Figure 10. Figure 10: Program-level well-formedness [PITH_FULL_IMAGE:figures/full_fig_p028_10.png]
Figure 11
Figure 11. Figure 11: Component-level typing. B.3 Declaration Declaration typing threads a typing environment through a component’s declaration block. The judgement Σ ; Γ ; Δ ⊢ 𝑝 ⇒ Γ′ checks a single declaration 𝑝 under signature Σ, effect environment Δ, and incoming environment Γ, extendi…
Figure 12
Figure 12. Figure 12: Declaration-level typing rules [PITH_FULL_IMAGE:figures/full_fig_p029_12.png]
Figure 13
Figure 13. Figure 13: Expression typing rules. C Side Conditions C.1 Typing – “causes” The “causes” judgement Δ ⊢ @𝑥 ⇒ 𝐹 reads “a change in 𝑥 is a sufficient cause for the effect 𝐹”. It is the side condition that ties the declared effect environment Δ to what a declaration may do: a state,…
Figure 14
Figure 14. Figure 14: The “causes” judgement. C.2 Sub-Effecting Sub-effecting is the subtyping relation 𝐹 ≤ 𝐹 ′ on effects, read “𝐹 is a sub-effect of 𝐹 ′ ”: anywhere an effect 𝐹 ′ is expected, an 𝐹 with 𝐹 ≤ 𝐹 ′ may be supplied. The rules propagate sub-effecting through the + and ∗ combina…
Figure 15
Figure 15. Figure 15: Sub-effecting. D Semantics D.1 External Scheduler Three new objects are added to the component-level housekeeping semantics. • ℰ, the external scheduler: an external scheduler presents an ordered list of event firings, each of the form (ℓ⟨𝑣1 ⟩, 𝑣2 ) where ℓ⟨𝑣1 ⟩ is th…
Figure 16
Figure 16. Figure 16: External tasks finishing. D.1.2 Listener-safe queues. A listener fires in response to an event, so it must not be able to inject a fresh labelled event back into the queue. It may, however, enqueue the internal housekeeping items: state updates, cancellations, listene…
Figure 17
Figure 17. Figure 17: Listener-safe queues. Lemma (Expression evaluation is listener-safe). If Σ ; 𝑉 ⊢ 𝑒 ⇓ 𝑣 ; 𝑈 , then ⊢ 𝑈 lsafe [PITH_FULL_IMAGE:figures/full_fig_p032_17.png]
Figure 18
Figure 18. Figure 18: Component-level stepping. (valid setteR) 𝑉 ′ = 𝑟 𝑒𝑚𝑜𝑣 𝑒𝑆𝑒𝑡𝑡𝑒𝑟 𝑠(𝑉 ) Σ ; 𝑉 ′ , 𝑥 = 𝑣 ⊢ 𝑒 ⇓ 𝑣′ ; ⋅ 𝑉𝑠 , 𝑥 = 𝑣 ⇒ 𝑠𝑒𝑡𝑡𝑒𝑟𝑥 (L𝜆𝑥.𝑒, 𝑉 M) ⇒ 𝑉𝑠 , 𝑥 = 𝑣′ [PITH_FULL_IMAGE:figures/full_fig_p034_18.png]
Figure 19
Figure 19. Figure 19: Setter validity. D.3 Declarations The declaration evaluation judgement Σ ; [𝑉𝑒 ∣ 𝑉𝑠 ] ; 𝑉 ; 𝑐 ⊢ 𝑝 ⇓ 𝑣 ; 𝑈 ; 𝑉 ′ is the big-step operational semantics of a declaration block. Under signature Σ, previous-render environment 𝑉𝑒 , and setter store 𝑉𝑠 , it evaluates the blo…
Figure 20
Figure 20. Figure 20: Declaration evaluation: vaR and RetuRn. D.3.1 Initialize. These rules give the first-render evaluation of state, effect, and subcomponent declarations, taken when the component is first mounted (the previous-render environments are empty, 𝑉𝑒 = 𝑉𝑠 = ⋅). A state declara…
Figure 21
Figure 21. Figure 21: Declaration evaluation: initialization. D.3.2 Rerender. These rules give the re-render evaluation of the same declaration forms, taken on every ren￾der after the first. They are distinguished from initialization by comparing the previous-render environment 𝑉𝑒 against …
Figure 22
Figure 22. Figure 22: Declaration evaluation: rerender. D.4 Expression The expression evaluation judgement Σ ; 𝑉 ⊢ 𝑒 ⇓ 𝑣 ; 𝑈 evaluates expression 𝑒 in environment 𝑉 to a value 𝑣, collecting into the update queue 𝑈 every side-effecting item the evaluation produces — setter applications, can…
Figure 23
Figure 23. Figure 23: Expression evaluation. E Instrumented Semantics E.1 Declarations The instrumented declaration judgement Γ ; 𝑋 ; 𝑉𝑠 ; 𝑉 ; 𝑐 ⊢Σ 𝑝 ⇓ 𝑣 ; 𝑇 ; 𝑉 ′ mirrors the ordinary declaration semantics but additionally records a trace 𝑇 — a structured log of the render with one entry …
Figure 24
Figure 24. Figure 24: Instrumented declaration evaluation: vaR and RetuRn. E.1.1 Rerender. These are the re-render rules of the instrumented semantics, the trace-producing counterparts of the re-render rules of the ordinary semantics. An effect block that fires (its watched set meets the c…
Figure 25
Figure 25. Figure 25: Instrumented declaration evaluation: rerender. F Preservation F.1 Values and Types These rules define when a runtime value is well-typed. The value-typing judgement Σ ⊧ 𝑣 ∶ 𝜏 assigns a closed value 𝑣 its type 𝜏 (closures also carry the latent effect 𝐹 of their body), …
Figure 26
Figure 26. Figure 26: Value typing [PITH_FULL_IMAGE:figures/full_fig_p038_26.png]
Figure 27
Figure 27. Figure 27: Value environment typing. F.2 Side Conditions F.2.1 Typing Update Queues. We first give the precise effect of a single queue item, one rule per kind of event the queue may carry, then assemble the effect of a whole queue with tq nil and tq cons. Subtyping (including ∗…
Figure 28
Figure 28. Figure 28: Queue-item typing: single events. Queue assembly. (tq nil) ⋅ ⊧𝑒 ⋅ (tq cons) 𝐹1 ⊧𝑒 𝑒 𝐹2 ⊧𝑒 𝑈 𝐹1 ∗ 𝐹2 ⊧𝑒 𝑒, 𝑈 [PITH_FULL_IMAGE:figures/full_fig_p039_28.png]
Figure 29
Figure 29. Figure 29: Queue-item typing: queue assembly. F.2.2 Derived from Subtyping Relations. These two rules extend queue-item typing to whole queues using the sub-effecting structure of effects. tq-meRge types a concatenated queue with the product of its parts’ effects, and tq-picK le…
Figure 30
Figure 30. Figure 30: Queue typing derived from subtyping. Lemma (Listen typing inversion). If 𝐹 ′ ⊧𝑒 𝑈 and listen(ℓ⟨𝑣 ⟩, 𝑐, 𝑚, 𝐹 ) ∈ 𝑈 , then Σ ⊧ 𝑐 ∶ Σ𝐸(ℓ⟨𝑣 ⟩) → unit ∣ 𝐹 [PITH_FULL_IMAGE:figures/full_fig_p039_30.png]
Figure 31
Figure 31. Figure 31: Justifying traces. F.2.4 Justifying Variable Change Sets. The change-set judgement (Δ, 𝑋1 ) ≻ 𝑇 ≻ 𝑋2 computes, from a trace 𝑇 evaluated under the incoming changed set 𝑋1 , the set 𝑋2 of variables whose state was actually changed during that render. It reads the setter…
Figure 32
Figure 32. Figure 32: Justifying variable change sets. F.2.5 Flush Queue. The flush-queue judgment threads the component state (𝑋 , 𝑉𝑠 , ℒ, 𝒞)through an update queue 𝑈 , applying each item to the appropriate carrier: setters update 𝑉𝑠 and 𝑋, cancels extend 𝒞, removes reset listener buckets…
Figure 33
Figure 33. Figure 33: Flush-queue judgment [PITH_FULL_IMAGE:figures/full_fig_p041_33.png]
Figure 34
Figure 34. Figure 34: Instrumented well-typed configuration. (Init) 𝐴 ∶ (comp A (𝑥 ∶ 𝜏 ) ∶ 𝜏𝑟 { 𝑝 }, Δ, Γ𝑠 ) ∈ Σ Γ𝑠 ; ∅ ; ⋅ ; 𝑥 = 𝑣 ; ‶" ⊢Σ 𝑝 ⇓ 𝑣𝑟 ; 𝑇 ; 𝑉 ⋅ → ⟨Σ; Δ; Γ𝑠 ∣∣ (∅, ∅, 𝑉 , ∅, ∅) ∣ A ∣ 𝑥 = 𝑣 ∣ rendered ∣ ⋅ ∣ 𝑇 ⟩ (No Updates) ⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮 ∣ A ∣ 𝑥 = 𝑣 ∣ rendered ∣ 𝑇1 ∣ RET 𝑦 ⟩ → …
Figure 35
Figure 35. Figure 35: Configuration stepping: initialization and flushing. (FiRe Cancel) 𝒮 = (𝑋1 , 𝑋2 , 𝑉𝑠 , ℒ, 𝒞) 𝒮 ′ = (𝑋1 , 𝑋2 , 𝑉𝑠 , ℒ, 𝒞 ′ ) 𝒞(ℓ⟨𝑣1 ⟩) ≥ 1 𝒞 ′ = 𝒞 ∖ { ℓ⟨𝑣1 ⟩ } ⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮 ∣ A ∣ 𝑥 = 𝑣 ∣ rendered ∣ 𝑇1 ∣ FIRE (ℓ⟨𝑣1 ⟩, 𝑣2 ), 𝑇2 ⟩ → ⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮 ′ ∣ A ∣ 𝑥 = 𝑣 ∣ render…
Figure 36
Figure 36. Figure 36: Configuration stepping: event firing. (waiting to RendeRed) 𝐴 ∶ (comp A (𝑥 ∶ 𝜏 ) ∶ 𝜏𝑟 { 𝑝 }, Δ, Γ𝑠 ) ∈ Σ 𝒮 = (𝑋1 , 𝑋2 , 𝑉𝑠1, ℒ, 𝒞) 𝒮 ′ = (𝑋2 ∪ {𝑥𝑖 ∣ 𝑣1𝑖 ≠ 𝑣2𝑖}, {𝑥𝑖 ∣ 𝑣1𝑖 ≠ 𝑣2𝑖}, 𝑉𝑠2, ℒ, 𝒞) Γ𝑠 ; 𝑋2 ∪ {𝑥𝑖 ∣ 𝑣1𝑖 ≠ 𝑣2𝑖} ; 𝑉𝑠1 ; 𝑥 = 𝑣2 ; ‶" ⊢Σ 𝑝 ⇓ 𝑣𝑟 ; 𝑇2 ; 𝑉𝑠2 ∃𝑖 𝑠.𝑡. 𝑣1…
Figure 37
Figure 37. Figure 37: Configuration stepping: re-rendering [PITH_FULL_IMAGE:figures/full_fig_p043_37.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

42 extracted references · 11 canonical work pages

  1. [1]

    Danel Ahman. 2023. When Programs Have to Watch Paint Dry. InFoundations of Software Science and Computation Structures, Orna Kupferman and Pawel Sobocinski (Eds.). Springer Nature Switzerland, Cham, 1–23.doi:10.1007/978- 3-031-30829-1_1 1:26 wunder, Das, and Gaboardi

    doi:10.1007/978- 2023

  2. [2]

    SimplyRaTT:afitch-stylemodalcalculus forreactiveprogrammingwithoutspaceleaks

    PatrickBahr,ChristianUldalGraulund,andRasmusEjlersMøgelberg.2019. SimplyRaTT:afitch-stylemodalcalculus forreactiveprogrammingwithoutspaceleaks. Proceedings of the ACM on Programming Languages3,ICFP(July2019), 1–27. doi:10.1145/3341713

    work page doi:10.1145/3341713 2019

  3. [3]

    Graphicaluserinterface(GUI)testing:Systematic mapping and repository.Information and Software Technology 55, 10 (Oct

    IshanBanerjee,BaoNguyen,VahidGarousi,andAtifMemon.2013. Graphicaluserinterface(GUI)testing:Systematic mapping and repository.Information and Software Technology 55, 10 (Oct. 2013), 1679–1694.doi:10.1016/j.infsof.2013. 03.004

    work page doi:10.1016/j.infsof.2013 2013

  4. [4]

    Gérard Berry and Georges Gonthier. 1992. The ESTEREL synchronous programming language: design, semantics, implementation. Sci. Comput. Program. 19, 2 (Nov. 1992), 87–152.doi:10.1016/0167-6423(92)90005-V

    doi:10.1016/0167-6423(92)90005-v 1992

  5. [5]

    Aloïs Brunel, Marco Gaboardi, Damiano Mazza, and Steve Zdancewic. 2014. A Core Quantitative Coeffect Calculus. In Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings (Lecture Note...

    doi:10.1007/978-3- 2014

  6. [6]

    Lin Clark and React Team. 2017. React Fiber Architecture.https://github.com/acdlite/react-fiber-architecture

    2017

  7. [7]

    Cooper and Shriram Krishnamurthi

    Gregory H. Cooper and Shriram Krishnamurthi. 2006. Embedding dynamic dataflow in a call-by-value language. In Proceedings of the 15th European Conference on Programming Languages and Systems (Vienna, Austria)(ESOP’06). Springer-Verlag, Berlin, Heidelberg, 294–308.doi:10.1007/11693024_20

    work page doi:10.1007/11693024_20 2006

  8. [8]

    Patrick Cousot. 2019. Abstract Semantic Dependency. InStatic Analysis - 26th International Symposium, SAS 2019, Porto, Portugal, October 8-11, 2019, Proceedings (Lecture Notes in Computer Science, Vol. 11822) , Bor-Yuh Evan Chang (Ed.). Springer, 389–410.doi:10.1007/978-3-030-32304-2_19

    work page doi:10.1007/978-3-030-32304-2_19 2019

Show all 42 references
  1. [9]

    Evan Czaplicki. 2012. Elm : Concurrent FRP for Functional GUIs.https://www.semanticscholar.org/paper/Elm-%3A- Concurrent-FRP-for-Functional-GUIs-Czaplicki/1791a8a278b83c54425d7581cb45320feba5f4b0

    2012

  2. [10]

    Parallelcomplexityanalysiswithtemporalsessiontypes

    AnkushDas,JanHoffmann,andFrankPfenning.2018. Parallelcomplexityanalysiswithtemporalsessiontypes. Proc. ACM Program. Lang. 2, ICFP (July 2018), 91:1–91:30.doi:10.1145/3236786

    2018 doi

  3. [11]

    Camil Demetrescu, Irene Finocchi, and Andrea Ribichini. 2011. Reactive imperative programming with dataflow constraints.In Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications (OOPSLA ’11) . Association for Comp...

    2011

  4. [12]

    Denning and Peter J

    Dorothy E. Denning and Peter J. Denning. 1977. Certification of Programs for Secure Information Flow.Commun. ACM 20, 7 (1977), 504–513.doi:10.1145/359636.359712

    1977

  5. [13]

    Conal Elliott and Paul Hudak. 1997. Functional reactive animation. InProceedings of the second ACM SIGPLAN in- ternational conference on Functional programming (ICFP ’97) . Association for Computing Machinery, New York, NY, USA, 263–273. doi:10.1145/258948.258973

    1997

  6. [14]

    Ottenstein, and Joe D

    Jeanne Ferrante, Karl J. Ottenstein, and Joe D. Warren. 1987. The Program Dependence Graph and Its Use in Opti- mization. ACM Transactions on Programming Languages and Systems 9, 3 (1987), 319–349.doi:10.1145/24039.24041

    1987

  7. [15]

    Simon Fowler. 2019. Model-View-Update-Communicate: Session Types meet the Elm Architecture.doi:10.48550/ ARXIV.1910.11108 Version Number: 3

    2019 doi arXiv

  8. [16]

    Event-DrivenMultipartySessionActors

    SimonFowlerandRaymondHu.2017. Event-DrivenMultipartySessionActors. Presentedatthe11thACMSIGPLAN Workshop on Higher-Order Programming with Effects (HOPE 2023). No proceedings

    2017

  9. [17]

    Ghica and Alex I

    Dan R. Ghica and Alex I. Smith. 2014. Bounded Linear Types in a Resource Semiring. InProgramming Languages and Systems, Zhong Shao (Ed.). Springer, Berlin, Heidelberg, 331–350.doi:10.1007/978-3-642-54833-8_18

    2014 doi

  10. [18]

    Jean-Yves Girard, Andre Scedrov, and Philip J. Scott. 1992. Bounded linear logic: a modular approach to polynomial- time computability. Theoretical Computer Science 97, 1 (April 1992), 1–66.doi:10.1016/0304-3975(92)90386-T

    1992 doi

  11. [19]

    Google. 2020. Largest Contentful Paint (LCP). web.dev.https://web.dev/articles/lcp. Core Web Vitals metric for perceived load speed; sites should target LCP of 2.5 seconds or less

    2020

  12. [20]

    Christian Uldal Graulund, Dmitrij Szamozvancev, and Neel Krishnaswami. 2021. Adjoint Reactive GUI Programming. In Foundations of Software Science and Computation Structures , Stefan Kiefer and Christine Tasson (Eds.). Vol. 12650. Springer International Publishing, Cham, 289–30...

    2021 doi

  13. [21]

    ThesynchronousdataflowprogramminglanguageLUSTRE

    N.Halbwachs,P.Caspi,P.Raymond,andD.Pilaud.1991. ThesynchronousdataflowprogramminglanguageLUSTRE. Proc. IEEE 79, 9 (1991), 1305–1320.doi:10.1109/5.97300

    1991 doi

  14. [22]

    Gilles Kahn. 1974. The Semantics of a Simple Language for Parallel Programming. InIFIP Congress. https://api. semanticscholar.org/CorpusID:18030506

    1974

  15. [23]

    Ohad Kammar, Sam Lindley, and Nicolas Oury. 2013. Handlers in action. InProceedings of the 18th ACM SIGPLAN international conference on Functional programming (ICFP ’13). Association for Computing Machinery, New York, NY, USA, 145–158. doi:10.1145/2500365.2500590 A Type-and-Ef...

    2013

  16. [24]

    Shin-yaKatsumata.2014. Parametriceffectmonadsandsemanticsofeffectsystems.In The 41st Annual ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014 , Suresh Jagannathan and Peter Sewell (Eds.). ACM, 633–646.doi:10...

    2014

  17. [25]

    David Khourshid. 2022. Goodbye, useEffect. Reactathon 2022 Conference Talk, Real World React (YouTube).https: //www.youtube.com/watch?v=HPoC-k7Rxwo

    2022

  18. [26]

    Krishnaswami and Nick Benton

    Neelakantan R. Krishnaswami and Nick Benton. 2011. Ultrametric Semantics of Reactive Programs. In2011 IEEE 26th Annual Symposium on Logic in Computer Science . IEEE, Toronto, ON, Canada, 257–266.doi:10.1109/LICS.2011.38

    2011 doi

  19. [27]

    Jay Lee, Joongwon Ahn, and Kwangkeun Yi. 2025. React-tRace: A Semantics for Understanding React Hooks.doi:10. 1145/3763067 arXiv:2507.05234 [cs]

    2025 arXiv

  20. [28]

    Sam Lindley, Conor McBride, and Craig McLaughlin. 2017. Do be do be do. doi:10.48550/arXiv.1611.09259 arXiv:1611.09259 [cs]

    2017 doi arXiv

  21. [29]

    Magnus Madsen, Ondřej Lhoták, and Frank Tip. 2020. A Semantics for the Essence of React. InLIPIcs, Volume 166, ECOOP 2020, Vol. 166. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 12:1–12:26.doi:10.4230/LIPICS.ECOOP. 2020.12 Artwork Size: 26 pages, 814986 bytes Medium: app...

    2020 doi

  22. [30]

    GUItesting:pitfallsandprocess

    A.M.Memon.2002. GUItesting:pitfallsandprocess. Computer 35,8(Aug.2002),87–88. doi:10.1109/MC.2002.1023795

    2002 arXiv

  23. [31]

    Meta Platforms. 2013. React: A JavaScript Library for Building User Interfaces.https://react.dev

    2013

  24. [32]

    Meta Platforms. 2024. React Compiler.https://react.dev/learn/react-compiler/introduction

    2024

  25. [33]

    Cooper,Michael Greenberg,Aleks Bromfield,andShriram Krishnamurthi.2009

    LeoA.Meyerovich,ArjunGuha, JacobBaskin, GregoryH. Cooper,Michael Greenberg,Aleks Bromfield,andShriram Krishnamurthi.2009. Flapjax:aprogramminglanguageforAjaxapplications.In Proceedings of the 24th ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Appl...

    2009

  26. [34]

    Stefan K. Muller. 2022. Static prediction of parallel computation graphs.Proc. ACM Program. Lang. 6, POPL (Jan. 2022), 46:1–46:31.doi:10.1145/3498708

    2022 doi

  27. [35]

    Rachit Nigam, Pedro Henrique Azevedo de Amorim, and Adrian Sampson. 2023. Modular Hardware Design with Timeline Types. Proc. ACM Program. Lang. 7, PLDI (June 2023), 120:343–120:367.doi:10.1145/3591234

    2023 doi

  28. [36]

    Amir Pnueli. 1977. The temporal logic of programs. InProceedings of the 18th Annual Symposium on Foundations of Computer Science (SFCS ’77). IEEE Computer Society, USA, 46–57.doi:10.1109/SFCS.1977.32

    1977 doi

  29. [37]

    Francis Rinaldi, june wunder, Arthur Azevedo de Amorim, and Stefan K. Muller. 2024. Pipelines and Beyond: Graph Types for ADTs with Futures.Proc. ACM Program. Lang. 8, POPL (Jan. 2024), 17:482–17:511.doi:10.1145/3632859

    2024 doi

  30. [38]

    Rosenband

    Daniel L. Rosenband. 2004. The ephemeral history register: flexible scheduling for rule-based designs. InProceedings of the Second ACM/IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE ’04).IEEE Computer Society, USA, 189–198.doi:10.1109/MEMCOD...

    2004 arXiv

  31. [39]

    TemporalVerificationwithAnswer-EffectModification:DependentTemporal Type-and-Effect System with Delimited Continuations

    TaroSekiyamaandHiroshiUnno.2023. TemporalVerificationwithAnswer-EffectModification:DependentTemporal Type-and-Effect System with Delimited Continuations. Proc. ACM Program. Lang. 7, POPL (Jan. 2023), 71:2079– 71:2110. doi:10.1145/3571264

    2023 doi

  32. [40]

    Taro Sekiyama and Hiroshi Unno. 2025. Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order Programs. Proc. ACM Program. Lang. 9, POPL (Jan. 2025), 78:2306–78:2336.doi:10.1145/3704914

    2025 doi

  33. [41]

    Sam Van den Vonder, Joeri De Koster, Florian Myter, and Wolfgang De Meuter. 2017. Tackling the awkward squad for reactive programming: the actor-reactor model. InProceedings of the 4th ACM SIGPLAN International Workshop on Reactive and Event-Based Languages and Systems (REBLS ...

    2017

  34. [42]

    causes” The “causes

    Zhanyong Wan and Paul Hudak. 2000. Functional reactive programming from first principles. InProceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation (Vancouver, British Columbia, Canada) (PLDI ’00). Association for Computing Machinery, N...

    2000

Pith tools

Reviewed July 30, 2026 · model on record in the stance chip above.