{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:33:56Z","timestamp":1781238836047,"version":"3.54.1"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2024,8,15]],"date-time":"2024-08-15T00:00:00Z","timestamp":1723680000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-2348706"],"award-info":[{"award-number":["CCF-2348706"]}],"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":[[2024,8,15]]},"abstract":"<jats:p>Cyber-Physical Systems (CPS) consist of software interacting with the physical world, such as robots, vehicles, and industrial processes. CPS are frequently responsible for the safety of lives, property, or the environment, and so software correctness must be determined with a high degree of certainty. To that end, simply testing a CPS is insufficient, as its interactions with the physical world may be difficult to predict, and unsafe conditions may not be immediately obvious. Formal verification can provide stronger safety guarantees but relies on the accuracy of the verified system in representing the real system. Bringing together verification and implementation can be challenging, as languages that are typically used to implement CPS are not easy to formally verify, and languages that lend themselves well to verification often abstract away low-level implementation details. Translation between verification and implementation languages is possible, but requires additional assurances in the translation process and increases software complexity; having both in a single language is desirable. This paper presents a formalization of MARVeLus, a CPS language which combines verification and implementation. We develop a metatheory for its synchronous refinement type system and demonstrate verified synchronous programs executing on real systems.<\/jats:p>","DOI":"10.1145\/3674657","type":"journal-article","created":{"date-parts":[[2024,8,15]],"date-time":"2024-08-15T12:49:04Z","timestamp":1723726144000},"page":"938-972","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Synchronous Programming with Refinement Types"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5461-6711","authenticated-orcid":false,"given":"Jiawei","family":"Chen","sequence":"first","affiliation":[{"name":"University of Michigan, Ann Arbor, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1576-2492","authenticated-orcid":false,"given":"Jos\u00e9 Luiz Vargas","family":"de Mendon\u00e7a","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0095-2146","authenticated-orcid":false,"given":"Bereket Shimels","family":"Ayele","sequence":"additional","affiliation":[{"name":"Addis Ababa Institute of Technology, Addis Ababa, Ethiopia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3537-3988","authenticated-orcid":false,"given":"Bereket Ngussie","family":"Bekele","sequence":"additional","affiliation":[{"name":"Addis Ababa Institute of Technology, Addis Ababa, Ethiopia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1535-5579","authenticated-orcid":false,"given":"Shayan","family":"Jalili","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, United States"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8217-173X","authenticated-orcid":false,"given":"Pranjal","family":"Sharma","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-3220-6099","authenticated-orcid":false,"given":"Nicholas","family":"Wohlfeil","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3134-1284","authenticated-orcid":false,"given":"Yicheng","family":"Zhang","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6378-1447","authenticated-orcid":false,"given":"Jean-Baptiste","family":"Jeannin","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,8,15]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57318-6_30"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2014.7040372"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_3"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386009"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_3"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/2562059.2562125"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/2038642.2038664"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192406"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632912"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45653-8_34"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062358"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/2461328.2461348"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/5.97299"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/41625.41641"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/232627.232651"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00050-7"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_29"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","unstructured":"Jiawei Chen Jos\u00e9 Luiz Vargas de Mendon\u00e7a Bereket Shimels Ayele Bereket Ngussie Bekele Shayan Jalili Pranjal Sharma Nicholas Wohlfeil Yicheng Zhang and Jean-Baptiste Jeannin. 2024. Synchronous Programming with Refinement Types. https:\/\/doi.org\/10.48550\/arXiv.2406.06221 10.48550\/arXiv.2406.06221 arXiv:2406.06221 [cs]. Extended version.","DOI":"10.48550\/arXiv.2406.06221"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","unstructured":"Jiawei Chen Jos\u00e9 Luiz Vargas de Mendon\u00e7a Bereket Shimels Ayele Bereket Ngussie Bekele Shayan Jalili Pranjal Sharma Nicholas Wohlfeil Yicheng Zhang and Jean-Baptiste Jeannin. 2024. Synchronous Programming with Refinement Types. https:\/\/doi.org\/10.5281\/zenodo.12702677 10.5281\/zenodo.12702677 Artifact.","DOI":"10.5281\/zenodo.12702677"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3563822.3568015"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/1176887.1176899"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2017.8285623"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45309-1_16"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498701"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.06.021"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290374"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_19"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428300"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA40945.2020.9196513"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2008.ECP.19"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1109\/5.97300"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08587-6_22"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1561\/2500000032"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3447928.3456633"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21437-0_6"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1109\/SOSCYPS.2016.7580000"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.2015.7170931"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/1-4020-8141-3_34"},{"key":"e_1_3_1_42_2","unstructured":"Ioannis Parissis. 1996. Test de logiciels synchrones sp\u00e9cifi\u00e9s en Lustre. Ph. D. Dissertation. Universit\u00e9 Joseph-Fourier- Grenoble I. https:\/\/theses.hal.science\/tel-00005010v1\/document"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/bxh138"},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9103-8"},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63588-0"},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24743-2_32"},{"key":"e_1_3_1_48_2","unstructured":"Christophe Ratel. 1992. D\u00e9finition et R\u00e9alisation d\u2019un Outil de V\u00e9rification Formelle de Programmes LUSTRE: le Syst\u00e8me LESAR. Ph. D. Dissertation. Universit\u00e9 Joseph Fourier. https:\/\/tel.archives-ouvertes.fr\/file\/index\/docid\/341223\/filename\/Ratel.Christophe_1992_these.pdf"},{"key":"e_1_3_1_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_3_1_50_2","doi-asserted-by":"publisher","unstructured":"Astrid Rupp Markus Tranninger Raffael Wallner Jasmina Zubaca Martin Steinberger and Martin Horn. 2019. Fast and low-cost testing of advanced driver assistance systems using small-scale vehicles. IFAC-PapersOnLine 52 5 (2019) 34\u201339. https:\/\/doi.org\/10.1016\/j.ifacol.2019.09.006 10.1016\/j.ifacol.2019.09.006","DOI":"10.1016\/j.ifacol.2019.09.006"},{"key":"e_1_3_1_51_2","doi-asserted-by":"publisher","DOI":"10.1109\/AQTR.2010.5520862"},{"key":"e_1_3_1_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_3_1_53_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-7091-9459-1_3"},{"key":"e_1_3_1_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_3_1_55_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSMCC.2011.2157682"},{"key":"e_1_3_1_56_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3674657","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3674657","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T07:50:35Z","timestamp":1770191435000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3674657"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,8,15]]},"references-count":55,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2024,8,15]]}},"alternative-id":["10.1145\/3674657"],"URL":"https:\/\/doi.org\/10.1145\/3674657","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,8,15]]},"assertion":[{"value":"2024-02-28","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-06-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-15","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}