{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,30]],"date-time":"2026-09-30T15:21:27Z","timestamp":1790781687204,"version":"4.1.0"},"reference-count":21,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF-1526109"],"award-info":[{"award-number":["CCF-1526109"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>The language Esterel has found success in many safety-critical applications, such as fly-by-wire systems and nuclear power plant control software. Its imperative style is natural to programmers building such systems and its precise semantics makes it work well for reasoning about programs.<\/jats:p>\n                  <jats:p>Existing semantics of Esterel generally fall into two categories: translation to Boolean circuits, or operational semantics that give a procedure for running a whole program. In contrast, equational theories enable reasoning about program behavior via equational rewrites at the source level. Such theories form the basis for proofs of transformations inside compilers or for program refactorings, and defining program evaluation syntactically.<\/jats:p>\n                  <jats:p>This paper presents the first such equational calculus for Esterel. It also illustrates the calculus\u2019s usefulness with a series of example equivalences and discuss how it enabled us to find bugs in Esterel implementations.<\/jats:p>","DOI":"10.1145\/3290374","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T08:33:51Z","timestamp":1546590831000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["A calculus for Esterel: if can, can. if no can, no can."],"prefix":"10.1145","volume":"3","author":[{"given":"Spencer P.","family":"Florence","sequence":"first","affiliation":[{"name":"Northwestern University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shu-Hung","family":"You","sequence":"additional","affiliation":[{"name":"Northwestern University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jesse A.","family":"Tov","sequence":"additional","affiliation":[{"name":"Northwestern University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Robert Bruce","family":"Findler","sequence":"additional","affiliation":[{"name":"Northwestern University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"North Holland","author":"Barendregt H.","year":"1984","unstructured":"H. Barendregt . The Lambda Calculus: its Syntax and Semantics . North Holland , 1984 . H. Barendregt. The Lambda Calculus: its Syntax and Semantics. North Holland, 1984."},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.97297"},{"key":"e_1_2_2_3_1","volume-title":"Robert de Simone. The Synchronous Languages 12 Years Later. Proceedings of the IEEE 91(1)","author":"Benveniste Albert","year":"2002","unstructured":"Albert Benveniste , Paul Caspi , Stephen A. Edwards , Nicolas Halbwachs , Paul Le Guernic , and Robert de Simone. The Synchronous Languages 12 Years Later. Proceedings of the IEEE 91(1) , 2002 . Albert Benveniste, Paul Caspi, Stephen A. Edwards, Nicolas Halbwachs, Paul Le Guernic, and Robert de Simone. The Synchronous Languages 12 Years Later. Proceedings of the IEEE 91(1), 2002."},{"key":"e_1_2_2_4_1","volume-title":"Sophia-Antipolis","author":"Berry G\u00e9rard","year":"2000","unstructured":"G\u00e9rard Berry . The Esterel v5 Language Primer Version v5_91. \u00c9cole des Mines de Paris, CMA and INRIA , Sophia-Antipolis , France , 2000 . G\u00e9rard Berry. The Esterel v5 Language Primer Version v5_91. \u00c9cole des Mines de Paris, CMA and INRIA, Sophia-Antipolis, France, 2000."},{"key":"e_1_2_2_5_1","series-title":"Draft Version 3","volume-title":"The Constructive Semantics of Pure Esterel","author":"Berry G\u00e9rard","year":"2002","unstructured":"G\u00e9rard Berry . The Constructive Semantics of Pure Esterel ( Draft Version 3 ) . 2002 . G\u00e9rard Berry. The Constructive Semantics of Pure Esterel (Draft Version 3). 2002."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(99)00015-5"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(92)90005-V"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2093328.2093337"},{"key":"e_1_2_2_9_1","volume-title":"Robert Bruce Findler, and Matthew Flatt. Semantics Engineering with PLT Redex","author":"Felleisen Matthias","year":"2009","unstructured":"Matthias Felleisen , Robert Bruce Findler, and Matthew Flatt. Semantics Engineering with PLT Redex . MIT Press , 2009 . Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt. Semantics Engineering with PLT Redex. MIT Press, 2009."},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90014-7"},{"key":"e_1_2_2_11_1","volume-title":"Racket","author":"Flatt Matthew","year":"2010","unstructured":"Matthew Flatt and PLT. Reference : Racket . PLT Inc., PLT-TR- 2010 -1, 2010. http:\/\/racket- lang.org\/tr1\/ Matthew Flatt and PLT. Reference: Racket. PLT Inc., PLT-TR-2010-1, 2010. http:\/\/racket- lang.org\/tr1\/"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814204.2814221"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2502323.2502326"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0144-6"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/509043"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"e_1_2_2_18_1","unstructured":"Dumitru Potop-Butucaru Stephen A. Edwards and G\u00e9rard Berry. Compiling Esterel. Springer 2007.   Dumitru Potop-Butucaru Stephen A. Edwards and G\u00e9rard Berry. Compiling Esterel. Springer 2007."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/502217.502226"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/647163.717691"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1216374.1216376"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290374","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290374","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290374","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:58:04Z","timestamp":1750193884000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290374"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":21,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290374"],"URL":"https:\/\/doi.org\/10.1145\/3290374","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}