A Semantics for the Essence of React

Authors Magnus Madsen , Ondřej Lhoták , Frank Tip

Thumbnail PDF


  • Filesize: 0.77 MB
  • 26 pages

Document Identifiers

Author Details

Magnus Madsen
  • Aarhus University, Denmark
Ondřej Lhoták
  • University of Waterloo, Canada
Frank Tip
  • Northeastern University, Boston, MA, USA


The authors are grateful to the anonymous reviewers for their insightful comments.

Cite AsGet BibTex

Magnus Madsen, Ondřej Lhoták, and Frank Tip. A Semantics for the Essence of React. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 12:1-12:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Traditionally, web applications have been written as HTML pages with embedded JavaScript code that implements dynamic and interactive features by manipulating the Document Object Model (DOM) through a low-level browser API. However, this unprincipled approach leads to code that is brittle, difficult to understand, non-modular, and does not facilitate incremental update of user-interfaces in response to state changes. React is a popular framework for constructing web applications that aims to overcome these problems. React applications are written in a declarative and object-oriented style, and consist of components that are organized in a tree structure. Each component has a set of properties representing input parameters, a state consisting of values that may vary over time, and a render method that declaratively specifies the subcomponents of the component. React’s concept of reconciliation determines the impact of state changes and updates the user-interface incrementally by selective mounting and unmounting of subcomponents. At designated points, the React framework invokes lifecycle hooks that enable programmers to perform actions outside the framework such as acquiring and releasing resources needed by a component. These mechanisms exhibit considerable complexity, but, to our knowledge, no formal specification of React’s semantics exists. This paper presents a small-step operational semantics that captures the essence of React, as a first step towards a long-term goal of developing automatic tools for program understanding, automatic testing, and bug finding for React web applications. To demonstrate that key operations such as mounting, unmounting, and reconciliation terminate, we define the notion of a well-behaved component and prove that well-behavedness is preserved by these operations.

Subject Classification

ACM Subject Classification
  • Theory of computation → Operational semantics
  • Software and its engineering → Semantics
  • JavaScript
  • React
  • operational semantics
  • lifecycle
  • reconciliation


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Preact: Fast 3kB alternative to React with the same modern API. https://preactjs.com/, 2019. Accessed: 2019-12-19.
  2. Vue.js: The progressive JavaScript framework. https://vuejs.org/, 2019. Accessed: 2019-12-19.
  3. Saba Alimadadi, Di Zhong, Magnus Madsen, and Frank Tip. Finding broken promises in asynchronous JavaScript programs. PACMPL, 2(OOPSLA):162:1-162:26, 2018. URL: https://doi.org/10.1145/3276532.
  4. Shay Artzi, Adam Kiezun, Julian Dolby, Frank Tip, Danny Dig, Amit M. Paradkar, and Michael D. Ernst. Finding bugs in web applications using dynamic test generation and explicit-state model checking. IEEE Trans. Software Eng., 36(4):474-494, 2010. URL: https://doi.org/10.1109/TSE.2010.31.
  5. SungGyeong Bae, Hyunghun Cho, Inho Lim, and Sukyoung Ryu. SAFEWAPI: Web API misuse detector for web applications. In Proceedings of the 22Nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2014, pages 507-517, New York, NY, USA, 2014. ACM. URL: https://doi.org/10.1145/2635868.2635916.
  6. Martin Bodin, Arthur Charguéraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudziuniene, Alan Schmitt, and Gareth Smith. A trusted mechanised JavaScript specification. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, pages 87-100, 2014. URL: https://doi.org/10.1145/2535838.2535876.
  7. Michel Bodin. Certified semantics and analysis of JavaScript. PhD thesis, Université de Rennes, 2017. Google Scholar
  8. Facebook, Inc. React: A JavaScript library for building user interfaces. https://www.reactjs.org/, 2019. Accessed: 2019-12-19.
  9. Philippa Gardner, Sergio Maffeis, and Gareth David Smith. Towards a program logic for JavaScript. In Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012, pages 31-44, 2012. URL: https://doi.org/10.1145/2103656.2103663.
  10. Arjun Guha, Claudiu Saftoiu, and Shriram Krishnamurthi. The essence of JavaScript. In Theo D'Hondt, editor, ECOOP 2010 - Object-Oriented Programming, 24th European Conference, Maribor, Slovenia, June 21-25, 2010. Proceedings, volume 6183 of Lecture Notes in Computer Science, pages 126-150. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14107-2_7.
  11. David Herman and Cormac Flanagan. Status report: specifying JavaScript with ML. In Proceedings of the 2007 workshop on Workshop on ML, pages 47-52. ACM, 2007. Google Scholar
  12. Facebook Inc. React native: Learn once, write anywhere. https://facebook.github.io/react-native/, 2019. Accessed: 2019-12-19.
  13. Matthew C. Loring, Mark Marron, and Daan Leijen. Semantics of asynchronous JavaScript. In Proceedings of the 13th ACM SIGPLAN International Symposium on on Dynamic Languages, Vancouver, BC, Canada, October 23 - 27, 2017, pages 51-62, 2017. URL: https://doi.org/10.1145/3133841.3133846.
  14. Magnus Madsen, Ondrej Lhoták, and Frank Tip. A model for reasoning about JavaScript promises. PACMPL, 1(OOPSLA):86:1-86:24, 2017. URL: https://doi.org/10.1145/3133910.
  15. Magnus Madsen, Ondřej Lhoták, and Frank Tip. A semantics for the essence of react. Technical Report CS-2020-03, University of Waterloo, 2020. URL: https://cs.uwaterloo.ca/sites/ca.computer-science/files/uploads/files/cs-2020-03.pdf.
  16. Magnus Madsen, Frank Tip, and Ondrej Lhoták. Static analysis of event-driven Node.js JavaScript applications. In Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, part of SPLASH 2015, Pittsburgh, PA, USA, October 25-30, 2015, pages 505-519, 2015. URL: https://doi.org/10.1145/2814270.2814272.
  17. Sergio Maffeis, John C. Mitchell, and Ankur Taly. An operational semantics for JavaScript. In G. Ramalingam, editor, Programming Languages and Systems, 6th Asian Symposium, APLAS 2008, Bangalore, India, December 9-11, 2008. Proceedings, volume 5356 of Lecture Notes in Computer Science, pages 307-325. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-89330-1_22.
  18. Frolin S. Ocariza Jr., Kartik Bajaj, Karthik Pattabiraman, and Ali Mesbah. A study of causes and consequences of client-side JavaScript bugs. IEEE Trans. Software Eng., 43(2):128-144, 2017. URL: https://doi.org/10.1109/TSE.2016.2586066.
  19. Frolin S. Ocariza Jr., Karthik Pattabiraman, and Ali Mesbah. Detecting inconsistencies in JavaScript MVC applications. In 37th IEEE/ACM International Conference on Software Engineering, ICSE 2015, Florence, Italy, May 16-24, 2015, Volume 1, pages 325-335, 2015. URL: https://doi.org/10.1109/ICSE.2015.52.
  20. Frolin S. Ocariza Jr., Karthik Pattabiraman, and Ali Mesbah. Detecting unknown inconsistencies in web applications. In Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, ASE 2017, Urbana, IL, USA, October 30 - November 03, 2017, pages 566-577, 2017. URL: https://doi.org/10.1109/ASE.2017.8115667.
  21. Daejun Park, Andrei Stefanescu, and Grigore Rosu. KJS: a complete formal semantics of JavaScript. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015, pages 346-356, 2015. URL: https://doi.org/10.1145/2737924.2737991.
  22. CACM Staff. React: Facebook’s functional turn on writing JavaScript. Commun. ACM, 59(12):56-62, 2016. URL: https://doi.org/10.1145/2980991.
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail