{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:43:59Z","timestamp":1780994639906,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":70,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,6,14]],"date-time":"2017-06-14T00:00:00Z","timestamp":1497398400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,6,14]]},"DOI":"10.1145\/3062341.3062358","type":"proceedings-article","created":{"date-parts":[[2017,6,14]],"date-time":"2017-06-14T10:01:04Z","timestamp":1497434464000},"page":"586-601","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":47,"title":["A formally verified compiler for Lustre"],"prefix":"10.1145","author":[{"given":"Timothy","family":"Bourke","sequence":"first","affiliation":[{"name":"Inria, France \/ ENS, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"L\u00e9lio","family":"Brun","sequence":"additional","affiliation":[{"name":"ENS, France \/ Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Pierre-\u00c9variste","family":"Dagand","sequence":"additional","affiliation":[{"name":"UPMC, France \/ CNRS, France \/ Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xavier","family":"Leroy","sequence":"additional","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marc","family":"Pouzet","sequence":"additional","affiliation":[{"name":"UPMC, France \/ ENS, France \/ Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lionel","family":"Rieg","sequence":"additional","affiliation":[{"name":"Coll\u00e8ge de France, France \/ Yale University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2017,6,14]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/2670099"},{"key":"e_1_3_2_1_3_1","volume-title":"Draft","author":"Auger C.","year":"2013","unstructured":"C. Auger , J.-L. Cola\u00e7o , G. Hamon , and M. Pouzet . A formalization and proof of a modular Lustre code generator . Draft , Jan. 2013 . C. Auger, J.-L. Cola\u00e7o, G. Hamon, and M. Pouzet. A formalization and proof of a modular Lustre code generator. Draft, Jan. 2013."},{"key":"e_1_3_2_1_4_1","series-title":"Lecture Notes in Computer Science","first-page":"46","volume-title":"8th IFIP WG 10.2 International Workshop on Software Technologies for Embedded and Ubiquitous Systems (SEUS","author":"Ballabriga C.","year":"2010","unstructured":"C. Ballabriga , H. Cass\u00e9 , C. Rochange , and P. Sainrat . OTAWA: An open toolbox for adaptive WCET analysis . In 8th IFIP WG 10.2 International Workshop on Software Technologies for Embedded and Ubiquitous Systems (SEUS 2010 ), volume 6399 of Lecture Notes in Computer Science , pages 35\u2013 46 , Waidhofen\/Ybbs, Austria, Oct . 2010. Springer . C. Ballabriga, H. Cass\u00e9, C. Rochange, and P. Sainrat. OTAWA: An open toolbox for adaptive WCET analysis. In 8th IFIP WG 10.2 International Workshop on Software Technologies for Embedded and Ubiquitous Systems (SEUS 2010), volume 6399 of Lecture Notes in Computer Science, pages 35\u201346, Waidhofen\/Ybbs, Austria, Oct. 2010. Springer."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2932189"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2038642.2038664"},{"key":"e_1_3_2_1_7_1","unstructured":"ACM Press.  ACM Press."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1967677.1967687"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375657.1375674"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9148-3"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_31"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-07512-9"},{"key":"e_1_3_2_1_13_1","unstructured":"Springer.  Springer."},{"key":"e_1_3_2_1_14_1","series-title":"Lecture Notes in Computer Science","first-page":"506","volume-title":"Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR","author":"Boulm\u00e9 S.","year":"2001","unstructured":"S. Boulm\u00e9 and G. Hamon . Certifying synchrony for free . In R. Nieuwenhuis and A. Voronkov, editors, Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2001 ), volume 2250 of Lecture Notes in Computer Science , pages 495\u2013 506 , Havana, Cuba, Dec . 2001. Springer . S. Boulm\u00e9 and G. Hamon. Certifying synchrony for free. In R. Nieuwenhuis and A. Voronkov, editors, Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2001), volume 2250 of Lecture Notes in Computer Science, pages 495\u2013506, Havana, Cuba, Dec. 2001. Springer."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/41625.41641"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/647399.724855"},{"key":"e_1_3_2_1_17_1","unstructured":"Springer.  Springer."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/780732.780754"},{"key":"e_1_3_2_1_19_1","volume-title":"Proceedings of the 14th International Conference on Software Engineering and Formal Methods (SEFM 2016","volume":"9763","author":"Champion A.","year":"2016","unstructured":"A. Champion , A. Gurfinkel , T. Kahsai , and C. Tinelli . Co-CoSpec: A mode-aware contract language for reactive systems. In R. De Nicola and E. K\u00fchn, editors , Proceedings of the 14th International Conference on Software Engineering and Formal Methods (SEFM 2016 ), volume 9763 of Lecture Notes in Computer Science, pages 347\u2013366, Vienna, Austria , July 2016 . A. Champion, A. Gurfinkel, T. Kahsai, and C. Tinelli. Co-CoSpec: A mode-aware contract language for reactive systems. In R. De Nicola and E. K\u00fchn, editors, Proceedings of the 14th International Conference on Software Engineering and Formal Methods (SEFM 2016), volume 9763 of Lecture Notes in Computer Science, pages 347\u2013366, Vienna, Austria, July 2016."},{"key":"e_1_3_2_1_20_1","unstructured":"Springer.  Springer."},{"key":"e_1_3_2_1_21_1","series-title":"Lecture Notes in Computer Science","first-page":"517","volume-title":"Proceedings of the 28th International Conference on Computer Aided Verification (CAV","author":"Champion A.","year":"2016","unstructured":"A. Champion , A. Mebsout , C. Sticksel , and C. Tinelli . The Kind 2 model checker . In S. Chaudhuri and A. Farzan, editors, Proceedings of the 28th International Conference on Computer Aided Verification (CAV 2016 ), Part II, volume 9780 of Lecture Notes in Computer Science , pages 510\u2013 517 , Toronto, Canada, July 2016. Springer . A. Champion, A. Mebsout, C. Sticksel, and C. Tinelli. The Kind 2 model checker. In S. Chaudhuri and A. Farzan, editors, Proceedings of the 28th International Conference on Computer Aided Verification (CAV 2016), Part II, volume 9780 of Lecture Notes in Computer Science, pages 510\u2013517, Toronto, Canada, July 2016. Springer."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/2584504"},{"key":"e_1_3_2_1_23_1","series-title":"Lecture Notes in Computer Science","first-page":"155","volume-title":"Proceedings of the 3rd International Conference on Embedded Software (EMSOFT","author":"Cola\u00e7o J.-L.","year":"2003","unstructured":"J.-L. Cola\u00e7o and M. Pouzet . Clocks as first class abstract types . In R. Alur and I. Lee, editors, Proceedings of the 3rd International Conference on Embedded Software (EMSOFT 2003 ), volume 2855 of Lecture Notes in Computer Science , pages 134\u2013 155 , Philadelphia , Pennsylvania, USA , Oct. 2003. J.-L. Cola\u00e7o and M. Pouzet. Clocks as first class abstract types. In R. Alur and I. Lee, editors, Proceedings of the 3rd International Conference on Embedded Software (EMSOFT 2003), volume 2855 of Lecture Notes in Computer Science, pages 134\u2013155, Philadelphia, Pennsylvania, USA, Oct. 2003."},{"key":"e_1_3_2_1_24_1","unstructured":"Springer.  Springer."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086228.1086261"},{"key":"e_1_3_2_1_26_1","series-title":"Lecture Notes in Computer Science","first-page":"108","volume-title":"Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics (TPHOLs","author":"Coupet-Grimal S.","year":"1999","unstructured":"S. Coupet-Grimal and L. Jakubiec . Hardware verification using co-induction in Coq . In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Th\u00e9ry, editors, Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 1999 ), volume 1690 of Lecture Notes in Computer Science , pages 91\u2013 108 , Nice , France, Sept . 1999. S. Coupet-Grimal and L. Jakubiec. Hardware verification using co-induction in Coq. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Th\u00e9ry, editors, Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 1999), volume 1690 of Lecture Notes in Computer Science, pages 91\u2013108, Nice, France, Sept. 1999."},{"key":"e_1_3_2_1_27_1","unstructured":"Springer.  Springer."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2695664.2695819"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2248418.2248426"},{"key":"e_1_3_2_1_30_1","volume-title":"Verilog SA","author":"Gimenez E.","year":"2000","unstructured":"E. Gimenez and E. Ledinot . Certification de SCADE V3. Rapport final du projet GENIE II , Verilog SA , Jan. 2000 . E. Gimenez and E. Ledinot. Certification de SCADE V3. Rapport final du projet GENIE II, Verilog SA, Jan. 2000."},{"key":"e_1_3_2_1_31_1","first-page":"9","volume-title":"Proceedings of the 8th International Conference on Formal Methods in Computer-Aided Design","author":"Hagen G.","year":"2008","unstructured":"G. Hagen and C. Tinelli . Scaling up the formal verification of Lustre programs with SMT-based techniques. In A. Cimatti and R. B. Jones, editors , Proceedings of the 8th International Conference on Formal Methods in Computer-Aided Design , pages 15:1\u201315: 9 , Portland, OR, USA , Nov. 2008 . IEEE. G. Hagen and C. Tinelli. Scaling up the formal verification of Lustre programs with SMT-based techniques. In A. Cimatti and R. B. Jones, editors, Proceedings of the 8th International Conference on Formal Methods in Computer-Aided Design, pages 15:1\u201315:9, Portland, OR, USA, Nov. 2008. IEEE."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/530328"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2006.24"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.97300"},{"key":"e_1_3_2_1_35_1","series-title":"Lecture Notes in Computer Science","first-page":"218","volume-title":"Proceedings of the 3rd International Symposium on Programming Language Implementation and Logic Programming (PLILP\u201991)","author":"Halbwachs N.","year":"1991","unstructured":"N. Halbwachs , P. Raymond , and C. Ratel . Generating efficient code from data-flow programs . In J. Maluszy\u00b4nski and M. Wirsing, editors, Proceedings of the 3rd International Symposium on Programming Language Implementation and Logic Programming (PLILP\u201991) , volume 528 of Lecture Notes in Computer Science , pages 207\u2013 218 , Passau, Germany, Aug. 1991 . Springer . N. Halbwachs, P. Raymond, and C. Ratel. Generating efficient code from data-flow programs. In J. Maluszy\u00b4nski and M. Wirsing, editors, Proceedings of the 3rd International Symposium on Programming Language Implementation and Logic Programming (PLILP\u201991), volume 528 of Lecture Notes in Computer Science, pages 207\u2013218, Passau, Germany, Aug. 1991. Springer."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.159839"},{"key":"e_1_3_2_1_37_1","volume-title":"Proceedings of the 6th International Symposium on Lucid and Intensional Programming (ISLIP\u201993)","author":"Halbwachs N.","year":"1993","unstructured":"N. Halbwachs , J.-C. Fernandez , and A. Bouajjani . An executable temporal logic to express safety properties and its connection with the language Lustre . In Proceedings of the 6th International Symposium on Lucid and Intensional Programming (ISLIP\u201993) , Quebec, Canada , Apr. 1993 . N. Halbwachs, J.-C. Fernandez, and A. Bouajjani. An executable temporal logic to express safety properties and its connection with the language Lustre. In Proceedings of the 6th International Symposium on Lucid and Intensional Programming (ISLIP\u201993), Quebec, Canada, Apr. 1993."},{"key":"e_1_3_2_1_38_1","series-title":"Lecture Notes in Computer Science","first-page":"112","volume-title":"Formal Development of Reactive Systems\u2014Case Study Production Cell","author":"Holenderski L.","unstructured":"L. Holenderski . Lustre . In C. Lewerentz and T. Lindner, editors, Formal Development of Reactive Systems\u2014Case Study Production Cell , volume 891 of Lecture Notes in Computer Science , chapter 6, pages 101\u2013 112 . Springer, Berlin, 1995. L. Holenderski. Lustre. In C. Lewerentz and T. Lindner, editors, Formal Development of Reactive Systems\u2014Case Study Production Cell, volume 891 of Lecture Notes in Computer Science, chapter 6, pages 101\u2013112. Springer, Berlin, 1995."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.375719"},{"key":"e_1_3_2_1_40_1","unstructured":"ACM Press.  ACM Press."},{"key":"e_1_3_2_1_41_1","volume-title":"Proceedings of the 4th European Congress on Embedded Real-Time Software (ERTS 2008","author":"Izerrouken N.","year":"2008","unstructured":"N. Izerrouken , X. Thirioux , M. Pantel , and M. Strecker . Certifying an automated code generator using formal tools: Preliminary experiments in the GeneAuto project . In Proceedings of the 4th European Congress on Embedded Real-Time Software (ERTS 2008 ). Soci\u00e9t\u00e9 des Ing\u00e9nieurs de l\u2019Automobile, Jan.\/ Feb. 2008 . N. Izerrouken, X. Thirioux, M. Pantel, and M. Strecker. Certifying an automated code generator using formal tools: Preliminary experiments in the GeneAuto project. In Proceedings of the 4th European Congress on Embedded Real-Time Software (ERTS 2008). Soci\u00e9t\u00e9 des Ing\u00e9nieurs de l\u2019Automobile, Jan.\/Feb. 2008."},{"key":"e_1_3_2_1_42_1","volume-title":"Verimag","author":"Jahier E.","year":"2016","unstructured":"E. Jahier , P. Raymond , and N. Halbwachs . The Lustre V6 Reference Manual . Verimag , Grenoble , Dec. 2016 . E. Jahier, P. Raymond, and N. Halbwachs. The Lustre V6 Reference Manual. Verimag, Grenoble, Dec. 2016."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_20"},{"key":"e_1_3_2_1_44_1","first-page":"475","volume-title":"Proceedings of the International Federation for Information Processing (IFIP) Congress","author":"Kahn G.","year":"1974","unstructured":"G. Kahn . The semantics of a simple language for parallel programming. In J. L. Rosenfeld, editor , Proceedings of the International Federation for Information Processing (IFIP) Congress 1974 , pages 471\u2013 475 . North-Holland, Aug. 1974. G. Kahn. The semantics of a simple language for parallel programming. In J. L. Rosenfeld, editor, Proceedings of the International Federation for Information Processing (IFIP) Congress 1974, pages 471\u2013475. North-Holland, Aug. 1974."},{"key":"e_1_3_2_1_45_1","first-page":"62","volume-title":"Proceedings of the 10th International Workshop on 2011, number 72 in Electronic Proceedings in Theoretical Computer Science","author":"Kahsai T.","year":"2011","unstructured":"T. Kahsai and C. Tinelli . PKIND: A parallel k-induction based model checker. In J. Barnat and K. Heljanko, editors , Proceedings of the 10th International Workshop on 2011, number 72 in Electronic Proceedings in Theoretical Computer Science , pages 55\u2013 62 , Snowbird, UT, USA , July 2011 . T. Kahsai and C. Tinelli. PKIND: A parallel k-induction based model checker. In J. Barnat and K. Heljanko, editors, Proceedings of the 10th International Workshop on 2011, number 72 in Electronic Proceedings in Theoretical Computer Science, pages 55\u201362, Snowbird, UT, USA, July 2011."},{"key":"e_1_3_2_1_46_1","series-title":"Lecture Notes in Computer Science","first-page":"337","volume-title":"Proceedings of the 3rd International Conference on Interactive Theorem Proving (ITP","author":"Klein G.","year":"2012","unstructured":"G. Klein , R. Kolanski , and A. Boyton . Mechanised separation algebra . In L. Beringer and A. Felty, editors, Proceedings of the 3rd International Conference on Interactive Theorem Proving (ITP 2012 ), volume 7406 of Lecture Notes in Computer Science , pages 332\u2013 337 , Princeton, NJ , USA , Aug. 2012. G. Klein, R. Kolanski, and A. Boyton. Mechanised separation algebra. In L. Beringer and A. Felty, editors, Proceedings of the 3rd International Conference on Interactive Theorem Proving (ITP 2012), volume 7406 of Lecture Notes in Computer Science, pages 332\u2013337, Princeton, NJ, USA, Aug. 2012."},{"key":"e_1_3_2_1_47_1","unstructured":"Springer.  Springer."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9099-0"},{"key":"e_1_3_2_1_50_1","volume-title":"Apr.","author":"Leroy X.","year":"2016","unstructured":"X. Leroy , D. Doligez , A. Frisch , J. Garrigue , D. R\u00e9my , and J. Vouillon . The OCaml system: Documentation and user\u2019s manual. Inria, 4.03 edition , Apr. 2016 . X. Leroy, D. Doligez, A. Frisch, J. Garrigue, D. R\u00e9my, and J. Vouillon. The OCaml system: Documentation and user\u2019s manual. Inria, 4.03 edition, Apr. 2016."},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480893"},{"key":"e_1_3_2_1_52_1","series-title":"Lecture Notes in Computer Science","first-page":"89","volume-title":"Proceedings of the 4th International Symposium on Formal Techniques for Real-Time and Fault-Tolerance (FTRTFT \u201996)","author":"Maraninchi F.","year":"1996","unstructured":"F. Maraninchi and N. Halbwachs . Compiling Argos into Boolean equations . In B. Jonsson and J. Parrow, editors, Proceedings of the 4th International Symposium on Formal Techniques for Real-Time and Fault-Tolerance (FTRTFT \u201996) , volume 1135 of Lecture Notes in Computer Science , pages 72\u2013 89 , Uppsala, Sweden, Sept. 1996 . Springer . F. Maraninchi and N. Halbwachs. Compiling Argos into Boolean equations. In B. Jonsson and J. Parrow, editors, Proceedings of the 4th International Symposium on Formal Techniques for Real-Time and Fault-Tolerance (FTRTFT \u201996), volume 1135 of Lecture Notes in Computer Science, pages 72\u201389, Uppsala, Sweden, Sept. 1996. Springer."},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(02)00093-X"},{"key":"e_1_3_2_1_54_1","volume-title":"The Mathworks","author":"Simulink Simulink\u2014Using","year":"2003","unstructured":"Simulink\u2014Using Simulink . The Mathworks , Natick, MA, U.S.A. , 5.1 edition, Sept. 2003 . Release 13SP1. Simulink\u2014Using Simulink. The Mathworks, Natick, MA, U.S.A., 5.1 edition, Sept. 2003. Release 13SP1."},{"key":"e_1_3_2_1_55_1","volume-title":"The Mathworks","author":"Reference Simulink","year":"2016","unstructured":"Simulink \u00ae Reference . The Mathworks , Natick, MA, U.S.A. , r 2016 b edition, Sept. 2016. Release 2016b. Simulink \u00ae Reference. The Mathworks, Natick, MA, U.S.A., r2016b edition, Sept. 2016. Release 2016b."},{"key":"e_1_3_2_1_56_1","series-title":"Lecture Notes in Computer Science","first-page":"80","volume-title":"Proceedings of the 35th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE","author":"Ngo V. C.","year":"2015","unstructured":"V. C. Ngo , J.-P. Talpin , and T. Gautier . Translation validation for synchronous data-flow specification in the SIGNAL compiler . In S. Graf and M. Viswanathan, editors, Proceedings of the 35th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2015 ), volume 9039 of Lecture Notes in Computer Science , pages 66\u2013 80 , Grenoble, France, June 2015. Springer . V. C. Ngo, J.-P. Talpin, and T. Gautier. Translation validation for synchronous data-flow specification in the SIGNAL compiler. In S. Graf and M. Viswanathan, editors, Proceedings of the 35th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2015), volume 9039 of Lecture Notes in Computer Science, pages 66\u201380, Grenoble, France, June 2015. Springer."},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/2764967.2775291"},{"key":"e_1_3_2_1_58_1","volume-title":"Proceedings of the 10th International Symposium on Practical Aspects of Declarative Languages (PADL 2008","author":"Pagano B.","year":"2008","unstructured":"B. Pagano , O. Andrieu , B. Canou , E. Chailloux , J.-L. Cola\u00e7o , T. Moniot , and P. Wang . Certified development tools implementation in Objective Caml. In P. Hudak and D. S. Warren, editors , Proceedings of the 10th International Symposium on Practical Aspects of Declarative Languages (PADL 2008 ), number 4902 in Lecture Notes in Computer Science, pages 2\u201317, San Francisco, CA, USA , Jan. 2008 . B. Pagano, O. Andrieu, B. Canou, E. Chailloux, J.-L. Cola\u00e7o, T. Moniot, and P. Wang. Certified development tools implementation in Objective Caml. In P. Hudak and D. S. Warren, editors, Proceedings of the 10th International Symposium on Practical Aspects of Declarative Languages (PADL 2008), number 4902 in Lecture Notes in Computer Science, pages 2\u201317, San Francisco, CA, USA, Jan. 2008."},{"key":"e_1_3_2_1_59_1","first-page":"413","volume-title":"Y. Bertot, G. Huet, J.-J","author":"Paulin-Mohring C.","unstructured":"C. Paulin-Mohring . A constructive denotational semantics for Kahn networks in Coq . In Y. Bertot, G. Huet, J.-J . L\u00e9vy, and G. Plotkin, editors, From Semantics to Computer Science : Essays in Honour of Gilles Kahn , pages 383\u2013 413 . Cambridge University Press, 2009. C. Paulin-Mohring. A constructive denotational semantics for Kahn networks in Coq. In Y. Bertot, G. Huet, J.-J. L\u00e9vy, and G. Plotkin, editors, From Semantics to Computer Science: Essays in Honour of Gilles Kahn, pages 383\u2013413. Cambridge University Press, 2009."},{"key":"e_1_3_2_1_60_1","series-title":"Lecture Notes in Computer Science","first-page":"246","volume-title":"Proceedings of the 25th International Colloquium on Automata, Languages and Programming","author":"Pnueli A.","unstructured":"A. Pnueli , M. Siegel , and O. Shtrichman . Translation validation for synchronous languages . In K. G. Larsen, S. Skyum, and G. Winskel, editors, Proceedings of the 25th International Colloquium on Automata, Languages and Programming , volume 1443 of Lecture Notes in Computer Science , pages 235\u2013 246 . Springer, 1998. A. Pnueli, M. Siegel, and O. Shtrichman. Translation validation for synchronous languages. In K. G. Larsen, S. Skyum, and G. Winskel, editors, Proceedings of the 25th International Colloquium on Automata, Languages and Programming, volume 1443 of Lecture Notes in Computer Science, pages 235\u2013246. Springer, 1998."},{"key":"e_1_3_2_1_61_1","volume-title":"Inria","author":"Pottier F.","year":"2016","unstructured":"F. Pottier and Y. R\u00e9gis-Gianas . Menhir Reference Manual . Inria , Aug. 2016 . F. Pottier and Y. R\u00e9gis-Gianas. Menhir Reference Manual. Inria, Aug. 2016."},{"key":"e_1_3_2_1_62_1","volume-title":"LRI","author":"Pouzet M.","year":"2006","unstructured":"M. Pouzet . Lucid Synchrone , version 3. Tutorial and reference manual. Universit\u00e9 Paris-Sud , LRI , Apr. 2006 . M. Pouzet. Lucid Synchrone, version 3. Tutorial and reference manual. Universit\u00e9 Paris-Sud, LRI, Apr. 2006."},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629335.1629365"},{"key":"e_1_3_2_1_65_1","volume-title":"Sept.","author":"Raymond P.","year":"1992","unstructured":"P. Raymond . The Lustre V4 distribution. http:\/\/wwwverimag.imag.fr\/The-Lustre-Toolbox.html , Sept. 1992 . P. Raymond. The Lustre V4 distribution. http:\/\/wwwverimag.imag.fr\/The-Lustre-Toolbox.html, Sept. 1992."},{"key":"e_1_3_2_1_66_1","series-title":"Lecture Notes in Computer Science","first-page":"347","volume-title":"F. Meyer auf der Heide and B","author":"Raymond P.","year":"1996","unstructured":"P. Raymond . Recognizing regular expressions by means of dataflow networks. In F. Meyer auf der Heide and B . Monien, editors, Proceedings of the 23rd International Colloquium on Automata, Languages and Programming, number 1099 in Lecture Notes in Computer Science , pages 336\u2013 347 , Paderborn, Germany, July 1996 . Springer . P. Raymond. Recognizing regular expressions by means of dataflow networks. In F. Meyer auf der Heide and B. Monien, editors, Proceedings of the 23rd International Colloquium on Automata, Languages and Programming, number 1099 in Lecture Notes in Computer Science, pages 336\u2013347, Paderborn, Germany, July 1996. Springer."},{"key":"e_1_3_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_57"},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/1017753.1017795"},{"key":"e_1_3_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.5555\/784820.784830"},{"key":"e_1_3_2_1_71_1","volume-title":"Inria","author":"Development Team The Coq","year":"2016","unstructured":"The Coq Development Team . The Coq proof assistant reference manual . Inria , 2016 . Version 8.5. The Coq Development Team. The Coq proof assistant reference manual. Inria, 2016. Version 8.5."},{"key":"e_1_3_2_1_72_1","volume-title":"LUCID, the dataflow programming language","author":"Wadge W. W.","year":"1985","unstructured":"W. W. Wadge and E. A. Ashcroft . LUCID, the dataflow programming language . Academic Press Professional, Inc. , 1985 . W. W. Wadge and E. A. Ashcroft. LUCID, the dataflow programming language. Academic Press Professional, Inc., 1985."}],"event":{"name":"PLDI '17: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Barcelona Spain","acronym":"PLDI '17","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3062341.3062358","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3062341.3062358","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:36:32Z","timestamp":1750203392000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3062341.3062358"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,6,14]]},"references-count":70,"alternative-id":["10.1145\/3062341.3062358","10.1145\/3062341"],"URL":"https:\/\/doi.org\/10.1145\/3062341.3062358","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3140587.3062358","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2017,6,14]]},"assertion":[{"value":"2017-06-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}