{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:43:58Z","timestamp":1780994638921,"version":"3.54.1"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,1]]},"abstract":"<jats:p>Specifications based on block diagrams and state machines are used to design control software, especially in the certified development of safety-critical applications. Tools like SCADE Suite and Simulink\/Stateflow are equipped with compilers that translate such specifications into executable code. They provide programming languages for composing functions over streams as typified by Dataflow Synchronous Languages like Lustre.<\/jats:p>\n          <jats:p>Recent work builds on CompCert to specify and verify a compiler for the core of Lustre in the Coq Interactive Theorem Prover. It formally links the stream-based semantics of the source language to the sequential memory manipulations of generated assembly code. We extend this work to treat a primitive for resetting subsystems. Our contributions include new semantic rules that are suitable for mechanized reasoning, a novel intermediate language for generating optimized code, and proofs of correctness for the associated compilation passes.<\/jats:p>","DOI":"10.1145\/3371112","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T19:45:25Z","timestamp":1576871125000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Mechanized semantics and verified compilation for a dataflow synchronous language with reset"],"prefix":"10.1145","volume":"4","author":[{"given":"Timothy","family":"Bourke","sequence":"first","affiliation":[{"name":"Inria, France \/ ENS, France \/ PSL University, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"L\u00e9lio","family":"Brun","sequence":"additional","affiliation":[{"name":"ENS, France \/ PSL University, France \/ Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marc","family":"Pouzet","sequence":"additional","affiliation":[{"name":"Sorbonne University, France \/ ENS, France \/ PSL University, France \/ Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11576280_32"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1450058.1450071"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICFEM.2000.873817"},{"key":"e_1_2_2_5_1","unstructured":"C\u00e9dric Auger Jean-Louis Cola\u00e7o Gregoire Hamon and Marc Pouzet. 2014. A Formalization and Proof of a Modular Lustre Code Generator. (2014). In preparation.  C\u00e9dric Auger Jean-Louis Cola\u00e7o Gregoire Hamon and Marc Pouzet. 2014. A Formalization and Proof of a Modular Lustre Code Generator. (2014). In preparation."},{"key":"e_1_2_2_6_1","volume-title":"Proc. 11th Int. Federation for Information Processing (IFIP) World Computer Congress, Gerhard Ritter (Ed.). Int. Federation for Information Processing (IFIP)","author":"Berry G\u00e9rard","year":"1989","unstructured":"G\u00e9rard Berry . 1989 . Real Time Programming: Special Purpose or General Purpose Languages . In Proc. 11th Int. Federation for Information Processing (IFIP) World Computer Congress, Gerhard Ritter (Ed.). Int. Federation for Information Processing (IFIP) , San Francisco, USA, 11\u201317. https:\/\/hal.inria.fr\/inria- 00075494\/document G\u00e9rard Berry. 1989. Real Time Programming: Special Purpose or General Purpose Languages. In Proc. 11th Int. Federation for Information Processing (IFIP) World Computer Congress, Gerhard Ritter (Ed.). Int. Federation for Information Processing (IFIP), San Francisco, USA, 11\u201317. https:\/\/hal.inria.fr\/inria- 00075494\/document"},{"key":"e_1_2_2_7_1","volume-title":"Foundations of Software Technology and Theoretical Computer Science (LNCS)","author":"Berry G\u00e9rard","unstructured":"G\u00e9rard Berry . 1993. Preemption in Concurrent Systems . In Foundations of Software Technology and Theoretical Computer Science (LNCS) , R. K. Shyamasundar (Ed.), Vol. 761 . Springer , Bombay, India , 72\u201393. http:\/\/www- sop.inria.fr\/members\/ Gerard.Berry\/Papers\/preemption.zip G\u00e9rard Berry. 1993. Preemption in Concurrent Systems. In Foundations of Software Technology and Theoretical Computer Science (LNCS), R. K. Shyamasundar (Ed.), Vol. 761. Springer, Bombay, India, 72\u201393. http:\/\/www- sop.inria.fr\/members\/ Gerard.Berry\/Papers\/preemption.zip"},{"key":"e_1_2_2_8_1","unstructured":"G\u00e9rard Berry. 2000. The Esterel v5 Language Primer (5.91 ed.). Ecole des Mines and INRIA. http:\/\/www- sop.inria.fr\/ members\/Gerard.Berry\/Papers\/primer.zip  G\u00e9rard Berry. 2000. The Esterel v5 Language Primer (5.91 ed.). Ecole des Mines and INRIA. http:\/\/www- sop.inria.fr\/ members\/Gerard.Berry\/Papers\/primer.zip"},{"key":"e_1_2_2_9_1","unstructured":"G\u00e9rard Berry. 2002. The Constructive Semantics of Pure Esterel (draft version 3 ed.). Sophia-Antipolis France. http:\/\/wwwsop.inria.fr\/members\/Gerard.Berry\/Papers\/EsterelConstructiveBook.pdf  G\u00e9rard Berry. 2002. The Constructive Semantics of Pure Esterel (draft version 3 ed.). Sophia-Antipolis France. http:\/\/wwwsop.inria.fr\/members\/Gerard.Berry\/Papers\/EsterelConstructiveBook.pdf"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375657.1375674"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9148-3"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2248418.2248437"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062358"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3207719.3207732"},{"key":"e_1_2_2_15_1","volume-title":"Arguments cadenc\u00e9s dans un compilateur Lustre v\u00e9rifi\u00e9. In 30 i\u00e8mes Journ\u00e9es Francophones des Langages Applicatifs (JFLA","author":"Bourke Timothy","year":"2019","unstructured":"Timothy Bourke and Marc Pouzet . 2019. Arguments cadenc\u00e9s dans un compilateur Lustre v\u00e9rifi\u00e9. In 30 i\u00e8mes Journ\u00e9es Francophones des Langages Applicatifs (JFLA 2019 ), Nicolas Magaud and Zaynah Dargaye (Eds.). Les Rousses, Haut-Jura, France , 109\u2013124. https:\/\/hal.inria.fr\/hal- 02005639\/document Timothy Bourke and Marc Pouzet. 2019. Arguments cadenc\u00e9s dans un compilateur Lustre v\u00e9rifi\u00e9. In 30 i\u00e8mes Journ\u00e9es Francophones des Langages Applicatifs (JFLA 2019), Nicolas Magaud and Zaynah Dargaye (Eds.). Les Rousses, Haut-Jura, France, 109\u2013124. https:\/\/hal.inria.fr\/hal- 02005639\/document"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90326-B"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0066-4138(94)90015-9"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/41625.41641"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00050-7"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-010-0170-3"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICESS.2009.80"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-009-0108-9"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48628-4_3"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2380356.2380394"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086228.1086261"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2017.8285623"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45212-6_10"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0160-y"},{"key":"e_1_2_2_30_1","unstructured":"Coq Development Team. 2019. The Coq proof assistant reference manual. Inria. https:\/\/coq.inria.fr\/distrib\/current\/refman\/ v. 8.9.  Coq Development Team. 2019. The Coq proof assistant reference manual. Inria. https:\/\/coq.inria.fr\/distrib\/current\/refman\/ v. 8.9."},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2248418.2248426"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086228.1086260"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/351268.351300"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24721-0_17"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/235321.235322"},{"key":"e_1_2_2_37_1","unstructured":"Erwan Jahier Pascal Raymond and Nicolas Halbwachs. 2019. The Lustre V6 Reference Manual. Verimag Grenoble. http:\/\/www- verimag.imag.fr\/DIST- TOOLS\/SYNCHRONE\/lustre- v6\/doc\/lv6- ref- man.pdf  Erwan Jahier Pascal Raymond and Nicolas Halbwachs. 2019. The Lustre V6 Reference Manual. Verimag Grenoble. http:\/\/www- verimag.imag.fr\/DIST- TOOLS\/SYNCHRONE\/lustre- v6\/doc\/lv6- ref- man.pdf"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_20"},{"key":"e_1_2_2_39_1","volume-title":"Proc. Int. Federation for Information Processing (IFIP) Congress","author":"Kahn Gilles","year":"1974","unstructured":"Gilles Kahn . 1974 . The Semantics of a Simple Language for Parallel Programming . In Proc. Int. Federation for Information Processing (IFIP) Congress 1974, Jack L. Rosenfeld (Ed.). North-Holland, Stockholm, Sweden, 471\u2013475. https:\/\/perso.enstaparistech.fr\/~chapoutot\/various\/kahn_networks.pdf Gilles Kahn. 1974. The Semantics of a Simple Language for Parallel Programming. In Proc. Int. Federation for Information Processing (IFIP) Congress 1974, Jack L. Rosenfeld (Ed.). North-Holland, Stockholm, Sweden, 471\u2013475. https:\/\/perso.enstaparistech.fr\/~chapoutot\/various\/kahn_networks.pdf"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61648-9_35"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0096-0551(01)00016-9"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(02)00093-X"},{"key":"e_1_2_2_45_1","volume-title":"Proc. 35th IFIP WG 6.1 Int. Conf. on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2015)","volume":"9039","author":"Ngo Van Chan","year":"2015","unstructured":"Van Chan Ngo , Jean-Pierre Talpin , and Thierry Gautier . 2015 . Translation Validation for Synchronous Data-Flow Specification in the SIGNAL Compiler . In Proc. 35th IFIP WG 6.1 Int. Conf. on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2015) (LNCS), Susanne Graf and Mahesh Viswanathan (Eds.) , Vol. 9039 . Springer, Grenoble, France, 66\u201380. https:\/\/hal.inria.fr\/hal- 01767328 Van Chan Ngo, Jean-Pierre Talpin, and Thierry Gautier. 2015. Translation Validation for Synchronous Data-Flow Specification in the SIGNAL Compiler. In Proc. 35th IFIP WG 6.1 Int. Conf. on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2015) (LNCS), Susanne Graf and Mahesh Viswanathan (Eds.), Vol. 9039. Springer, Grenoble, France, 66\u201380. https:\/\/hal.inria.fr\/hal- 01767328"},{"key":"e_1_2_2_46_1","volume-title":"From Semantics to Computer Science: Essays in Honour of Gilles Kahn, Yves Bertot, G\u00e9rard Huet, Jean-Jacques L\u00e9vy, and Gordon Plotkin (Eds.). CUP","author":"Paulin-Mohring Christine","year":"1806","unstructured":"Christine Paulin-Mohring . 2009. A constructive denotational semantics for Kahn networks in Coq . In From Semantics to Computer Science: Essays in Honour of Gilles Kahn, Yves Bertot, G\u00e9rard Huet, Jean-Jacques L\u00e9vy, and Gordon Plotkin (Eds.). CUP , Cambridge , UK , 383\u2013413. https:\/\/hal.inria.fr\/inria- 0043 1806 \/document Christine Paulin-Mohring. 2009. A constructive denotational semantics for Kahn networks in Coq. In From Semantics to Computer Science: Essays in Honour of Gilles Kahn, Yves Bertot, G\u00e9rard Huet, Jean-Jacques L\u00e9vy, and Gordon Plotkin (Eds.). CUP, Cambridge, UK, 383\u2013413. https:\/\/hal.inria.fr\/inria- 00431806\/document"},{"key":"e_1_2_2_47_1","unstructured":"Simon Peyton Jones (Ed.). 2003. Haskell 98 Language and Libraries: The Revised Report. CUP Cambridge UK. https: \/\/www.haskell.org\/definition\/haskell98- report.pdf  Simon Peyton Jones (Ed.). 2003. Haskell 98 Language and Libraries: The Revised Report. CUP Cambridge UK. https: \/\/www.haskell.org\/definition\/haskell98- report.pdf"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-70628-3"},{"key":"e_1_2_2_49_1","unstructured":"Marc Pouzet. 2006. Lucid Synchrone v. 3. Tutorial and reference manual. Universit\u00e9 Paris-Sud. https:\/\/www.di.ens.fr\/ ~pouzet\/lucid- synchrone\/lucid- synchrone- 3.0- manual.pdf  Marc Pouzet. 2006. Lucid Synchrone v. 3. Tutorial and reference manual. Universit\u00e9 Paris-Sud. https:\/\/www.di.ens.fr\/ ~pouzet\/lucid- synchrone\/lucid- synchrone- 3.0- manual.pdf"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_57"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-C.2017.83"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11432-016-9270-0"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951924"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/1113830.1113834"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10626-010-0096-1"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24953-7_33"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/EMSOFT.2013.6658587"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371112","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371112","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:43Z","timestamp":1750273543000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371112"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":55,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1145\/3371112"],"URL":"https:\/\/doi.org\/10.1145\/3371112","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"2019-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}