{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:22:06Z","timestamp":1750220526761,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":57,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,8,22]],"date-time":"2021-08-22T00:00:00Z","timestamp":1629590400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"ANR","award":["ANR-13-BS02-0008"],"award-info":[{"award-number":["ANR-13-BS02-0008"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,8,27]]},"DOI":"10.1145\/3471872.3472970","type":"proceedings-article","created":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T01:21:27Z","timestamp":1629336087000},"page":"35-46","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["The w-calculus: a synchronous framework for the verified modelling of digital signal processing algorithms"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9299-1192","authenticated-orcid":false,"given":"Emilio Jes\u00fas","family":"Gallego Arias","sequence":"first","affiliation":[{"name":"Inria, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre","family":"Jouvelot","sequence":"additional","affiliation":[{"name":"MINES ParisTech, France \/ PSL University, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sylvain","family":"Ribstein","sequence":"additional","affiliation":[{"name":"n.n., n.n."}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dorian","family":"Desblancs","sequence":"additional","affiliation":[{"name":"ENS, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,8,22]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30494-4_4"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2005.857314"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_3_2_2_4_1","unstructured":"C\u00e9dric Auger. 2013. Compilation Certifi\u00e9e de SCADE\/LUSTRE. Universit\u00e9 Paris-Sud. http:\/\/tel.archives-ouvertes.fr\/tel-00818169\/ C\u00e9dric Auger. 2013. Compilation Certifi\u00e9e de SCADE\/LUSTRE. Universit\u00e9 Paris-Sud. http:\/\/tel.archives-ouvertes.fr\/tel-00818169\/"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24276-2_8"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2543581.2543591"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-07151-0_5"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2562059.2562125"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(91)90001-E"},{"volume-title":"Proof, Language, and Interaction, Essays in Honour of Robin Milner, Gordon D","author":"Berry G\u00e9rard","key":"e_1_3_2_2_10_1","unstructured":"G\u00e9rard Berry . 2000. The foundations of Esterel . In Proof, Language, and Interaction, Essays in Honour of Robin Milner, Gordon D . Plotkin, Colin Stirling, and Mads Tofte (Eds.). The MIT Press , 425\u2013454. isbn:978-0-262-16188-6 G\u00e9rard Berry. 2000. The foundations of Esterel. In Proof, Language, and Interaction, Essays in Honour of Robin Milner, Gordon D. Plotkin, Colin Stirling, and Mads Tofte (Eds.). The MIT Press, 425\u2013454. isbn:978-0-262-16188-6"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(92)90005-V"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(4:1)2012"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45653-8_34"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062358"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371112"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46663-6_4"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2461328.2461348"},{"key":"e_1_3_2_2_18_1","unstructured":"Timothy Bourke Pierre \u00c9variste Dagand Marc Pouzet and Lionel Rieg. 2017. Verifying clock-directed modular code generation for Lustre. In JFLA\u201917. Timothy Bourke Pierre \u00c9variste Dagand Marc Pouzet and Lionel Rieg. 2017. Verifying clock-directed modular code generation for Lustre. In JFLA\u201917."},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_19"},{"key":"e_1_3_2_2_20_1","article-title":"Ptolemy: A Framework for Simulating and Prototyping Heterogenous","author":"Buck Joseph T.","year":"1994","unstructured":"Joseph T. Buck , Soonhoi Ha , Edward A. Lee , and David G. Messerschmitt . 1994 . Ptolemy: A Framework for Simulating and Prototyping Heterogenous Systems. Int. Journal in Computer Simulation. Joseph T. Buck, Soonhoi Ha, Edward A. Lee, and David G. Messerschmitt. 1994. Ptolemy: A Framework for Simulating and Prototyping Heterogenous Systems. Int. Journal in Computer Simulation.","journal-title":"Journal in Computer Simulation."},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"crossref","unstructured":"Paul Caspi Gr\u00e9goire Hamon and Marc Pouzet. 2008. Synchronous functional programming: The Lucid Synchrone experiment. Real-Time Systems: Description and Verification Techniques: Theory and Tools.. Paul Caspi Gr\u00e9goire Hamon and Marc Pouzet. 2008. Synchronous functional programming: The Lucid Synchrone experiment. Real-Time Systems: Description and Verification Techniques: Theory and Tools..","DOI":"10.1002\/9780470611012.ch7"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/41625.41641"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/232627.232651"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411206"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/258948.258973"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951939"},{"key":"e_1_3_2_2_27_1","volume-title":"Proceedings of the 13th Linux Audio Conference. https:\/\/github.com\/ejgallego\/mini-faust-coq","author":"Gallego Arias Emilio Jes\u00fas","year":"2015","unstructured":"Emilio Jes\u00fas Gallego Arias , Pierre Jouvelot , and Olivier Hermant . 2015 . A Taste of Sound Reasoning in Faust . In Proceedings of the 13th Linux Audio Conference. https:\/\/github.com\/ejgallego\/mini-faust-coq Emilio Jes\u00fas Gallego Arias, Pierre Jouvelot, and Olivier Hermant. 2015. A Taste of Sound Reasoning in Faust. In Proceedings of the 13th Linux Audio Conference. https:\/\/github.com\/ejgallego\/mini-faust-coq"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217295.1217298"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22863-6_10"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(99)00023-4"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/11546382_2"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cl.2011.03.001"},{"key":"e_1_3_2_2_34_1","volume-title":"The Semantics of Simple Language for Parallel Programming. In IFIP Congress.","author":"Kahn Gilles","year":"1974","unstructured":"Gilles Kahn . 1974 . The Semantics of Simple Language for Parallel Programming. In IFIP Congress. Gilles Kahn. 1974. The Semantics of Simple Language for Parallel Programming. In IFIP Congress."},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009880"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500588"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2975980.2975983"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3330999"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1987.5009446"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596559"},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796811000153"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2015.07.002"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13321-3_17"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0144-6"},{"volume-title":"C\u00e9sar A","author":"Ls","key":"e_1_3_2_2_45_1","unstructured":"2008. TPHO Ls 2008 , Otmane A\u00eft Mohamed , C\u00e9sar A . Mu\u00f1oz, and Sofi\u00e8ne Tahar (Eds.). isbn:978-3-540-71065-3 2008. TPHOLs 2008, Otmane A\u00eft Mohamed, C\u00e9sar A. Mu\u00f1oz, and Sofi\u00e8ne Tahar (Eds.). isbn:978-3-540-71065-3"},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2000.855774"},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36388-2_25"},{"key":"e_1_3_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00500-004-0388-1"},{"key":"e_1_3_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3064899.3064902"},{"key":"e_1_3_2_2_50_1","unstructured":"Jos\u00e9 Luis Pino Soonhoi Ha Edward A Lee and Joseph T Buck. 1995. Software synthesis for DSP using Ptolemy. Jos\u00e9 Luis Pino Soonhoi Ha Edward A Lee and Joseph T Buck. 1995. Software synthesis for DSP using Ptolemy."},{"key":"e_1_3_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010027404223"},{"key":"e_1_3_2_2_52_1","doi-asserted-by":"crossref","unstructured":"Daniel Ricketts Gregory Malecha and Sorin Lerner. 2016. Modular Deductive Verification of Sampled-Data Systems. In EMSOFT. Daniel Ricketts Gregory Malecha and Sorin Lerner. 2016. Modular Deductive Verification of Sampled-Data Systems. In EMSOFT.","DOI":"10.1145\/2968478.2968495"},{"key":"e_1_3_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08970-6_31"},{"key":"e_1_3_2_2_54_1","unstructured":"Julius Orion Smith III. 2007. Introduction to Digital Filters: with Audio Applications. W3K Publishing. isbn:978-0974560717 https:\/\/ccrma.stanford.edu\/~jos\/filters\/ Julius Orion Smith III. 2007. Introduction to Digital Filters: with Audio Applications. W3K Publishing. isbn:978-0974560717 https:\/\/ccrma.stanford.edu\/~jos\/filters\/"},{"key":"e_1_3_2_2_55_1","volume-title":"Mathematics of the Discrete Fourier Transform (DFT): with Audio Applications","author":"Julius Orion","unstructured":"Julius Orion Smith III. 2007. Mathematics of the Discrete Fourier Transform (DFT): with Audio Applications ( 2 nd ed.). W3K Publishing . isbn:978-0974560748 https:\/\/ccrma.stanford.edu\/~jos\/mdft\/ Julius Orion Smith III. 2007. Mathematics of the Discrete Fourier Transform (DFT): with Audio Applications (2nd ed.). W3K Publishing. isbn:978-0974560748 https:\/\/ccrma.stanford.edu\/~jos\/mdft\/","edition":"2"},{"key":"e_1_3_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.mejo.2013.10.012"},{"key":"e_1_3_2_2_57_1","unstructured":"Sander Stuijk Marc Geilen and Twan Basten. 2006. SDF3: SDF For Free.. In ACSD. Sander Stuijk Marc Geilen and Twan Basten. 2006. SDF3: SDF For Free.. In ACSD."},{"key":"e_1_3_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45937-5_14"}],"event":{"name":"ICFP '21: 26th ACM SIGPLAN International Conference on Functional Programming","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Virtual Republic of Korea","acronym":"ICFP '21"},"container-title":["Proceedings of the 9th ACM SIGPLAN International Workshop on Functional Art, Music, Modelling, and Design"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3471872.3472970","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3471872.3472970","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:24:49Z","timestamp":1750195489000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3471872.3472970"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,22]]},"references-count":57,"alternative-id":["10.1145\/3471872.3472970","10.1145\/3471872"],"URL":"https:\/\/doi.org\/10.1145\/3471872.3472970","relation":{},"subject":[],"published":{"date-parts":[[2021,8,22]]},"assertion":[{"value":"2021-08-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}