Pith. sign in

REVIEW 3 major objections 4 minor 1 cited by

React-tRace: A Semantics for Understanding React Hooks

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

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

Pith's one-line read React-tRace supplies the first operational semantics for React's useState and useEffect Hooks, specifying exactly when component bodies re-evaluate, when Effects run, and when state updates trigger re-renders, and it provides proofs plus…

desk verdict A genuinely useful first semantics for React Hooks, with a documented but real caveat about the conformance tests' print-order claims; still deserves peer review. read the letter →

arxiv 2507.05234 v2 pith:44TV56NJ submitted 2025-07-07 cs.PL cs.SE

Jay Lee , Joongwon Ahn , Kwangkeun Yi This is my paper · ORCID
classification cs.PLcs.SE MSC 68Q5568N30
keywords ReactHooksoperationalsemanticsuseStateEffectrenderlifecyclereconciliationconformancetestingvisualizer
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

React-tRace claims to capture the essence of React's Hooks: it gives an operational semantics for useState and useEffect that fixes exactly when a component body is re-evaluated, when queued state updates are applied, and when Effects run. The authors prove that the semantics satisfies two documented properties of React: setter calls made during rendering trigger immediate re-evaluation, and Effects run after a re-render triggered by a state change in the view or an ancestor. They also validate the semantics with a 38-test suite run against React 16.14, 17.0.2, 18.3.1, and 19.1.0, reporting identical behavior except for one execution-order difference caused by React's same-state update optimization. If the claim holds, the opaque causes of common bugs such as infinite re-rendering and flickering become formally explainable, and tools like the accompanying visualizer can step through each render decision with precision.

What carries the argument

The load-bearing mechanism is the render loop, a transition system on global states with three modes: /react (rendered, awaiting Effect commit), check mode, and the event loop. Two auxiliaries carry the detail: the retrying evaluation of a component body, which re-runs the body whenever a setter call leaves a Check decision, and the Check and Effect decisions stored on each view in the tree memory, which determine whether Effects are committed and whether a re-render reconciles the child tree. This machinery answers the paper's central timing questions: a component body is re-evaluated exactly when Check is set, Effects run in post-order after a render exactly when Effect is set, and reconciliation happens only when the re-evaluated body still requests Effect.

What would settle it

Take the SelfCounter effect loop or any of the suite's scenarios and run it under React 19 in a concurrent mode, for example wrapped in a transition with Suspense, and compare the print order and render count with React-tRace's prediction; any divergence would refute the claim that the three-mode loop captures React's scheduling. A more local falsifier would be a conforming program in which React commits Effects before children's Effects, contrary to the post-order rule.

Watch

Extended reading notes

Core claim

On its own terms, the central discovery is that React's seemingly ad hoc Hook scheduling can be organized around a small three-mode render loop: after the initial render the runtime is in rendered mode, where queued Effects are committed; then in check mode, where the runtime scans for state updates and re-renders if needed; then in event-loop mode, where it waits for user input. Each component body is evaluated by a retrying big-step evaluation that re-reads the body whenever a setter call leaves a Check decision, and each view in the tree memory carries Check and Effect decisions plus a state store of queued update closures. The two most confusing Hook behaviors then fall out as theorems: a setter called during rendering forces immediate re-evaluation, and an Effect is committed exactly when a view's state or an ancestor's state genuinely changed or a setter ran during body evaluation. The paper also shows that the one deliberate divergence from real React, React's eager skipping of same-value updates, preserves program behavior for pure updater functions, so the semantics remains faithful for conforming applications.

Load-bearing premise

The argument assumes that the three-mode render loop with Check and Effect decisions fully determines React's observable scheduling of component re-evaluations and Effect commits, and that the only divergence from real React is the same-value eager-update optimization; in particular, concurrent rendering features such as transitions and Suspense are not modeled.

Editorial extensions

If this is right

  • A setter called in a component body forces the body to be read again with the queued update applied, so an unconditional top-level setter causes an infinite retry loop that never completes a render.
  • Effects are committed after a re-render only for views whose state or an ancestor's state changed, or whose body ran a setter; setting state in an Effect to the same value does not by itself cause a re-render.
  • React's skip-same-value update optimization can be ignored when reasoning about conforming applications, because Theorem 8 shows it preserves the final tree memory and only changes output when component bodies themselves print.
  • The 38-test conformance suite reproduces the same render counts, ordering, reconciliation behavior, and error behavior across React 16.14, 17.0.2, 18.3.1, and 19.1.0, so the semantics is version-independent for the modeled subset.
  • The definitional interpreter and visualizer can replay every render step, making infinite-render, flicker, and cross-component update bugs inspectable step by step.

Reading between the lines

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

  • Going beyond the paper: the three-mode loop could be parameterized by update timing and reactivity primitive to yield a comparative semantics across other reactive UI frameworks, a direction the paper sketches but does not develop.
  • Going beyond the paper: the Check and Effect decision sets could serve as abstract-interpretation lattice elements, enabling a static analyzer to flag infinite-retry and effect-loop bugs before runtime; the paper lists static analysis only as future work.
  • Going beyond the paper: adding a fourth mode for layout effects such as useLayoutEffect would give a testable extension whose render-order predictions could be checked against browser behavior.
  • Going beyond the paper: a direct empirical test of the concurrency boundary would be to run the same suite under React's transitions and Suspense, features the semantics deliberately leaves out, to see where the predictions stop matching.
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 / 4 minor

Summary. The paper introduces React-tRace, an operational semantics for a small functional language that models React's useState and useEffect Hooks. The semantics consists of a render loop with modes /react, check, and event-loop, a tree memory storing per-view state stores and effect queues, and big-step evaluation rules for component bodies, effects, event handlers, reconciliation, and retry-based re-evaluation. The authors prove two documentation-derived properties (Theorems 1 and 2), prove a similarity theorem bounding React's eager-update optimization (Theorem 8), and report an empirical conformance suite of 38 self-authored tests run against React 16.14, 17.0.2, 18.3.1, and 19.1.0. They also describe a definitional interpreter and a visualization tool.

Significance. If the conformance claims hold, React-tRace would be a useful foundation for analyzing and explaining React Hooks behavior, and the paper would make a solid contribution to the semantics of reactive UI frameworks. The operational rules are detailed and cover the render/re-render/effect lifecycle, including reconciliation and the retry mechanism; the proofs of Theorems 1, 2, and 8 are plausible though not machine-checked; and the artifact, test suite, and visualizer are publicly available, which is a strength. However, the empirical evidence is weaker than the prose suggests: the only acknowledged divergence from React is in the exact ordering of console output, and the test suite itself relies on console output from component bodies to observe render timing. That gap is load-bearing for the paper's central claim that React-tRace predicts when component bodies are re-evaluated and when Effects run.

major comments (3)
  1. [§6.1.2, §6.2, Table 1 (S17)] The acknowledged divergence from React is not minor relative to the paper's conformance claim. The Counter example in §6.1.2 shows React-tRace printing 0\0\1\2\3 while React prints 0\1\2\0\3, and Theorem 8 guarantees equal output only when component bodies do not print. Yet §6.2's tests use prints inside component bodies to count renders and observe effect timing, so the instrumented programs used for validation are exactly the class for which Theorem 8 provides no output-equality guarantee. Marking S17 as ✓† hides this divergence on the ordered console output that the paper itself treats as observable behavior (Print rule, Fig. 5; §2.1). The conformance claim should be restricted to final memory or render counts, or the semantics and tests should be extended to handle print-observable timing.
  2. [§4.2.1, §6.2] The paper does not specify whether the tests used React's legacy renderer or the default concurrent createRoot renderer in React 18/19. The render loop in Fig. 4 models a synchronous, non-interruptible engine with a single ordered mode sequence; React 18/19's concurrent scheduling and automatic batching can change when component bodies are evaluated relative to a strictly synchronous model. Since the central claim is that the model predicts when re-evaluations and Effects occur, the empirical section should report the rendering mode used in the React-side tests and explicitly state which concurrent features (transitions, Suspense, automatic batching outside events) are outside the model. Without this, the claimed conformance for React 18.3.1 and 19.1.0 is not fully established.
  3. [§6.2] The statement that the test suite 'covers all 44 evaluation rules' is not substantiated by the table. The 18 scenarios in Table 1 are presented as outcome-level comparisons, and the text notes that individual tests exercise multiple rules, but no mapping from tests to rules is given. Since the empirical section is the main external evidence for conformance, a rule-by-rule or scenario-by-rule coverage table would make the claim checkable.
minor comments (4)
  1. [Appendix A.2, handlers] In the definition of handlers, the clause for a path uses `m[p].children`, but views have a `child` field (defined in §4.1.2 and used throughout Figs. 7–10). This should be `m[p].child`.
  2. [§6.2] The paper does not state whether the React-side tests used `ReactDOM.render` or `createRoot`; this information should be reported because it determines whether concurrent rendering semantics are exercised.
  3. [Appendix B, Lemma 20 proof] There is a typo: 'componets print nothing' should be 'components print nothing'.
  4. [§2.1, Console example] The console output in §2.1 shows 'button /hand-p⌢int-up', which appears to be a rendering artifact; the notation should be clarified or replaced with a plain label.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: React-tRace's conformance claim rests on external empirical comparison against React releases, not on input-reproducing equations or self-citation chains.

full rationale

React-tRace's central claim is supported in two independent ways: internal theorems about the semantics (Theorems 1, 2, and 8) and an external test suite comparing the React-tRace interpreter against actual React releases (16.14.0, 17.0.2, 18.3.1, and 19.1.0). The theorems are internal consistency results that follow from the operational rules (e.g., Theorem 2's proof explicitly cites SttReBind and AppSetComp as the rules introducing the Effect decision), but the paper does not present them as empirical predictions about React; the external comparison is the load-bearing validation. There are no fitted parameters, no equations that reproduce their own inputs, and no derivation that reduces by construction to the target claim. The acknowledged discrepancy in §6.1.2 and Table 1, scenario S17, where React's eager-update optimization changes some execution orders and Theorem 8 guarantees output equality only when component bodies do not print, weakens the precision of the conformance claim, but it is an honestly stated limitation rather than a circular step. Self-citations (Lee 2025; Lee and Ahn 2025) are to a StackOverflow search and an artifact repository, and neither is load-bearing for the semantics or its validation. Therefore, no significant circularity is present.

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

The ledger records the domain assumptions under which React-tRace is claimed to model React. No free parameters are fitted. The invented entities (decision sets, tree memory) are the formal machinery itself; each has independent_evidence=False because it is only validated indirectly via the conformance suite, not by any prediction external to the model.

assumptions (5)
  • domain assumption A big-step semantics with explicit output buffers adequately models JavaScript component evaluation for the purposes of hook timing.
    Section 2 decouples from JS; Section 4.2 uses big-step evaluation. This assumes the omitted JS semantics (objects, prototypes, strict equality) do not affect render timing.
  • domain assumption The Rules of Hooks (calls only at the top level, unconditional order) are enforced syntactically and are sufficient for validity.
    Section 5 checks this during parsing; Definition 6 (validity) relies on the syntactic restriction. The paper treats this as a React requirement rather than a model artifact.
  • domain assumption Only useState and useEffect matter for the essence of hook behavior; other hooks, dependency arrays, and custom hooks are out of scope.
    Section 2 explicitly states this scoping choice and sketches extensions in Section 7.
  • domain assumption React's runtime scheduling is captured by the render-step relation with modes /react, check, and event-loop, and decisions Check/Effect; concurrent scheduling features do not alter observable behavior for the tested programs.
    Section 4.2.1 defines the loop; Section 6.1.2 acknowledges one optimization divergence but otherwise assumes equivalence. No analysis of React's concurrent mode (transitions, Suspense) is provided.
  • domain assumption State update functions passed to setters are pure, as required for Theorem 8.
    Definition 3 defines purity; the optimization-preservation proof (Theorem 8) depends on it. Real React also requires purity, so this is a documentation-derived assumption, but it is an added constraint on the model.
invented entities (2)
  • Decision set (dec) containing Check and Effect markers
    purpose: Records, per view, whether the component body must be retried (Check) and whether queued effects must run (Effect).
    Internal semantic machinery; no direct external evidence exists, and it is validated only indirectly through the conformance suite against React.
  • Tree memory (m) mapping paths to view records
    purpose: Models the mounted view hierarchy and per-view state/effect queues, allowing inter-component updates via paths.
    Formal device for the semantics; not directly observable in React. Its behavior is tested only through the interpreter's conformance tests.

how reviews work

0 comments
Cite this review

Pith. "Pith review of React-tRace: A Semantics for Understanding React Hooks." pith.science (2026). https://pith.science/paper/44TV56NJ

@misc{pith2026250705234,
  author       = {Pith},
  title        = {Pith review of: React-tRace: A Semantics for Understanding React Hooks},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/44TV56NJ}},
  note         = {Machine review of arXiv:2507.05234}
}
read the original abstract

React has become the most widely used web front-end framework, enabling the creation of user interfaces in a declarative and compositional manner. Hooks are a set of APIs that manage side effects in function components in React. However, their semantics are often seen as opaque to developers, leading to UI bugs. We introduce React-tRace, a formalization of the semantics of the essence of React Hooks, providing a semantics that clarifies their behavior. We demonstrate that our model captures the behavior of React, by theoretically showing that it embodies essential properties of Hooks and empirically comparing our React-tRace-definitional interpreter against a test suite. Furthermore, we showcase a practical visualization tool based on the formalization to demonstrate how developers can better understand the semantics of Hooks.

Figures

Figures reproduced from arXiv: 2507.05234 by the authors.

Figure 1
Figure 1. Syntax of React-tRace. • React-tRace is a foundation for building semantic-based tools. React-tRace provides a semantics for React Hooks (§4), which is the first step in designing any semantic-based tool, such as an abstract interpreter [Cousot and Cousot 1977; Rival and Yi 2020]. As an example for a semantic-based tool based on React-tRace, we present an interactive tool that explains and visualizes the behavior of… view at source ↗
Figure 2
Figure 2. Visualization of a tree memory and render step transitions for a simple recursive component. [PITH_FULL_IMAGE:figures/full_fig_p009_2.png] view at source ↗
Figure 3
Figure 3. Semantic function dependencies. • ⟨𝑒, 𝛿⟩ or ⟨𝑡,𝑚, 𝜔, 𝛿, 𝜇⟩ ↩→ ⟨𝑡,𝑚′ , 𝜔′ , 𝛿, 𝜇′ ⟩ is a render step transition ( [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗
Figures from the paper (8 more)
Figure 4
Figure 4. Figure 4: Render step transitions. Given a program 𝑃, the loop begins with an initial state ⟨𝑒, 𝛿⟩, where 𝑒 is the main expression of 𝑃 and 𝛿 is the definition table of all components defined in 𝑃. Note that the definition table 𝛿 and the root tree 𝑡 (once initialized) remain un…
Figure 5
Figure 5. Figure 5: Evaluation of an expression (an excerpt). [PITH_FULL_IMAGE:figures/full_fig_p012_5.png]
Figure 6
Figure 6. Figure 6: Retrying evaluation of a component body. [PITH_FULL_IMAGE:figures/full_fig_p013_6.png]
Figure 7
Figure 7. Figure 7: Initialization of a view spec. 4.2.3 Initial Render. When a view is initially rendered, it is initialized from a view spec ( [PITH_FULL_IMAGE:figures/full_fig_p014_7.png]
Figure 8
Figure 8. Figure 8: Committing Effects. 𝑚, 𝛿 ⊢ check(𝑡) = ⟨𝜇,𝑚′ , 𝜔⟩ CheckConst 𝑚, 𝛿 ⊢ check(𝑘) = ⟨•,𝑚, []⟩ CheckClos 𝑚, 𝛿 ⊢ check(𝑐𝑙) = ⟨•,𝑚, []⟩ CheckArray [PITH_FULL_IMAGE:figures/full_fig_p015_8.png]
Figure 9
Figure 9. Figure 9: Checking a tree for re-render. Proc. ACM Program. Lang., Vol. 9, No. OOPSLA2, Article 289. Publication date: October 2025 [PITH_FULL_IMAGE:figures/full_fig_p015_9.png]
Figure 10
Figure 10. Figure 10: Reconciliation of a tree with a view spec. [PITH_FULL_IMAGE:figures/full_fig_p016_10.png]
Figure 11
Figure 11. Figure 11: The React-tRace interpreter and visualizer interface, showing the illustrative example from §4.3. (b) The previous child ⟨⟩ is reconciled with the closure view spec ⟨𝜆_.setS f, _⟩ (Check￾Effect). (c) The closure view spec is initialized as it is of different type with…

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

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

    cs.PL 2026-07 conditional novelty 7.0 of 10

    Willow tracks render and event timing as graded effects, proves preservation, and uses the resulting temporal dependency graphs to statically detect cascades, loops, and stale listeners in React-like programs.

Reference graph

Works this paper leans on

36 extracted references · 25 canonical work pages · cited by 1 Pith paper

  1. [6]

    https://dioxuslabs.com/learn/0.6/reference/hooks/

    Hooks and component state. https://dioxuslabs.com/learn/0.6/reference/hooks/. Accessed: 2025-03-25. Conal Elliott and Paul Hudak

    work page 2025

  2. [14]

    A Model for Reasoning About JavaScript Promises. Proc. ACM Program. Lang. 1, OOPSLA, Article 86 (Oct. 2017), 24 pages. doi:10.1145/3133910 Magnus Madsen, Ondřej Lhoták, and Frank Tip

    work page doi:10.1145/3133910 2017

  3. [24]

    InProceedings of the 8th Symposium on Dynamic Languages (Tucson, Arizona, USA) (DLS ’12)

    A Tested Semantics for Getters, Setters, and Eval in JavaScript. InProceedings of the 8th Symposium on Dynamic Languages (Tucson, Arizona, USA) (DLS ’12). Association for Computing Machinery, New York, NY, USA, 1–16. doi:10.1145/2384577.2384579 Pranjal

    work page arXiv

  4. [25]

    https://stackoverflow.com/q/54069253

    The useState set method is not reflecting a change immediately. https://stackoverflow.com/q/54069253. Accessed: 2025-03-24. Gabriel Radanne, Vasilis Papavasileiou, Jérôme Vouillon, and Vincent Balat. 2016a. Eliom: tierless Web programming from the ground up. In Proceedings of the 28th Symposium on the Implementation and Application of Functional Programmi...

    work page arXiv 2025

  5. [26]

    JavaScript Language Design and Implementation in Tandem. Commun. ACM 67, 5 (May 2024), 86–95. doi:10.1145/3624723 Manuel Serrano, Erick Gallesio, and Florian Loitsch

    doi:10.1145/3624723 2024

  6. [27]

    https://survey.stackoverflow.co/2024/

    2024 Stack Overflow Developer Survey. https://survey.stackoverflow.co/2024/. Accessed: 2025-01-21. CACM Staff

    work page 2024

  7. [28]

    React: Facebook’s Functional Turn on Writing JavaScript. Commun. ACM 59, 12 (Dec. 2016), 56–62. doi:10.1145/2980991 Quoc Van Tang

    work page doi:10.1145/2980991 2016

  8. [29]

    https://stackoverflow

    React hooks useState setValue still rerender one more time when value is equal. https://stackoverflow. com/q/57652176. Accessed: 2025-03-24. Tehila

    work page arXiv 2025

Show all 36 references
  1. [30]

    https: //stackoverflow.com/q/74034014

    Updating state to the same value directly in the component body during render causes infinite loop. https: //stackoverflow.com/q/74034014. Accessed: 2025-03-24. vadirn

    2025

  2. [31]

    Accessed: 2025-03-24

    Does React batch state update functions when using hooks? https://stackoverflow.com/q/53048495. Accessed: 2025-03-24. Lorenzo Veronese, Benjamin Farinier, Pedro Bernardo, Mauro Tempesta, Marco Squarcina, and Matteo Maffei

    2025

  3. [34]

    ACM Comput

    A Survey of Multitier Programming. ACM Comput. Surv. 53, 4, Article 81 (Sept. 2020), 35 pages. doi:10.1145/3397495 Proc. ACM Program. Lang., Vol. 9, No. OOPSLA2, Article

    2020 doi

  4. [35]

    counter") 5 return Button(

    289:42 Jay Lee, Joongwon Ahn, and Kwangkeun Yi 11 console.log(count); 12 } 13 </script> 14 <button on:click={h}> 15 {count} 16 </button> C.9 SwiftUI counter gets printed every render. count updates are immediate. 1 struct Counter: View { 2 @State private var count = 0 3 var bo...

    2025

  5. [166]

    Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 12:1–12:26

    , Robert Hirschfeld and Tobias Pape (Eds.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 12:1–12:26. doi:10.4230/LIPIcs.ECOOP.2020.12 Sergio Maffeis, John C. Mitchell, and Ankur Taly

    2020 doi

  6. [247]

    Brandenburg, Guy Vidal-Naquet, and Martin Wirsing (Eds.)

    , Franz J. Brandenburg, Guy Vidal-Naquet, and Martin Wirsing (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 22–39. doi:10.1007/BFb0039592 Jay Lee

    doi

  7. [289]

    Publication date: October 2025

    2025

  8. [1977]

    In Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (Los Angeles, California) (POPL ’77)

    Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (Los Angeles, California) (POPL ’77). Association for C...

  9. [1997]

    In Proceedings of the Second ACM SIGPLAN International Conference on Functional Programming (Amsterdam, The Netherlands) (ICFP ’97)

    Functional Reactive Animation. In Proceedings of the Second ACM SIGPLAN International Conference on Functional Programming (Amsterdam, The Netherlands) (ICFP ’97). Association for Computing Machinery, New York, NY, USA, 263–273. doi:10.1145/258948.258973 Richard Feldman

  10. [2007]

    In Formal Methods for Components and Objects (FMCO ’06) (Lecture Notes in Computer Science, Vol

    Links: Web Programming Without Tiers. In Formal Methods for Components and Objects (FMCO ’06) (Lecture Notes in Computer Science, Vol. 4709), Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem-Paul de Roever (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg...

    doi

  11. [2009]

    In Proceedings of the 24th ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications (Orlando, Florida, USA) (OOPSLA ’09)

    Flapjax: A Programming Language for Ajax Applications. In Proceedings of the 24th ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications (Orlando, Florida, USA) (OOPSLA ’09). Association for Computing Machinery, New York, NY, USA, 1–20. doi:10...

  12. [2010]

    In ECOOP 2010 – Object-Oriented Programming (Lecture Notes in Computer Science, Vol

    The Essence of JavaScript. In ECOOP 2010 – Object-Oriented Programming (Lecture Notes in Computer Science, Vol

    2010

  13. [2012]

    ACM Trans

    Reasoning about Web Applications: An Operational Semantics for HOP. ACM Trans. Program. Lang. Syst. 34, 2, Article 10 (June 2012), 40 pages. doi:10.1145/2220365.2220369 Adam Chlipala. 2015a. An Optimizing Compiler for a Purely Functional Web-Application Language. In Proceeding...

    2012

  14. [2013]

    In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (Seattle, Washington, USA) (PLDI ’13)

    Asynchronous Functional Reactive Programming for GUIs. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (Seattle, Washington, USA) (PLDI ’13). Association for Computing Machinery, New York, NY, USA, 411–422. doi:10.1145/249195...

  15. [2014]

    From bytecode to JavaScript: the Js_of_ocaml compiler. Softw. Pract. Exper. 44, 8 (Aug. 2014), 951–972. doi:10.1002/spe.2187 Pascal Weisenburger, Johannes Wirth, and Guido Salvaneschi

    2014 doi

  16. [2015]

    In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (Portland, OR, USA) (PLDI ’15)

    KJS: A Complete Formal Semantics of JavaScript. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (Portland, OR, USA) (PLDI ’15). Association for Computing Machinery, New York, NY, USA, 346–356. doi:10.1145/2737924.2737991 Jihy...

  17. [2016]

    In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (Amsterdam, Netherlands) (OOPSLA ’16)

    Automated Reasoning for Web Page Layout. In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (Amsterdam, Netherlands) (OOPSLA ’16). Association for Computing Machinery, New York, NY, USA, 181–194....

    2016 doi

  18. [2017]

    JaVerT: JavaScript Verification Toolchain. Proc. ACM Program. Lang. 2, POPL, Article 50 (Dec. 2017), 33 pages. doi:10.1145/3158138 Arjun Guha, Claudiu Saftoiu, and Shriram Krishnamurthi

    2017 doi

  19. [2018]

    In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (Philadelphia, PA, USA) (PLDI ’18)

    Verifying That Web Pages Have Accessible Layout. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (Philadelphia, PA, USA) (PLDI ’18). Association for Computing Machinery, New York, NY, USA, 1–14. doi:10.1145/3192366.3192407 Pa...

  20. [2019]

    Modular Verification of Web Page Layout. Proc. ACM Program. Lang. 3, OOPSLA, Article 151 (Oct. 2019), 26 pages. doi:10.1145/3360577 Pavel Panchekha, Adam T. Geller, Michael D. Ernst, Zachary Tatlock, and Shoaib Kamil

    2019 doi

  21. [2020]

    166), Robert Hirschfeld and Tobias Pape (Eds.)

    (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 166), Robert Hirschfeld and Tobias Pape (Eds.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 14:1–14:28. doi:10.4230/LIPIcs.ECOOP.2020.14 José Fragoso Santos, Petar Maksimović, Daiva Naud...

    2020 doi

  22. [2021]

    In Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering (Virtual Event, Australia) (ASE ’20)

    JISET: JavaScript IR-based Semantics Extraction Toolchain. In Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering (Virtual Event, Australia) (ASE ’20). Association for Computing Machinery, New York, NY, USA, 647–658. doi:10.1145/3324884....

  23. [2022]

    https://facebook.github.io/jsx/

    JSX. https://facebook.github.io/jsx/. Accessed: 2025-03-24. Meta Platforms, Inc. 2025a. Component – React. https://react.dev/reference/react/Component. Accessed: 2025-03-12. Meta Platforms, Inc. 2025b. Higher-Order Components – React. https://legacy.reactjs.org/docs/higher-ord...

    2025

  24. [2023]

    In 2023 IEEE Symposium on Security and Privacy (SP ’23)

    WebSpec: Towards Machine-Checked Analysis of Browser Security Mechanisms. In 2023 IEEE Symposium on Security and Privacy (SP ’23). IEEE, San Francisco, CA, USA, 2761–2779. doi:10.1109/sp46215.2023.10179465 Jérôme Vouillon and Vincent Balat

    2023

  25. [2024]

    A Core Calculus for Documents: Or, Lambda: The Ultimate Document. Proc. ACM Program. Lang. 8, POPL, Article 23 (Jan. 2024), 28 pages. doi:10.1145/3632865 Evan Czaplicki and Stephen Chong

    2024 doi

  26. [2025]

    useEffect

    A screenshot of the StackOverflow search results of ‘"useEffect" "infinite"’. https://archive.org/details/useeffect- infinite. Accessed: 2025-03-24. Proc. ACM Program. Lang., Vol. 9, No. OOPSLA2, Article

    2025

  27. [5356]

    Springer Berlin Heidelberg, Berlin, Heidelberg, 307–325

    , Ganesan Ramalingam (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 307–325. doi:10.1007/978-3-540-89330-1_22 Meta Platforms, Inc

    doi

  28. [6183]

    Springer Berlin Heidelberg, Berlin, Heidelberg, 126–150

    , Theo D’Hondt (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 126–150. doi:10.1007/978-3-642-14107-2_7 Gilles Kahn

    doi

Pith tools

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