{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:48:08Z","timestamp":1775868488840,"version":"3.50.1"},"reference-count":75,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"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":["2211996 and 2211997"],"award-info":[{"award-number":["2211996 and 2211997"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-21-1-0385"],"award-info":[{"award-number":["FA9550-21-1-0385"]}],"id":[{"id":"10.13039\/100000181","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":[[2025,1,7]]},"abstract":"<jats:p>\n                    Many of today\u2019s message-passing systems not only require messages to be exchanged in a certain order but also to happen at a certain\n                    <jats:italic toggle=\"yes\">time<\/jats:italic>\n                    or within a certain\n                    <jats:italic toggle=\"yes\">time window<\/jats:italic>\n                    . Such correctness conditions are particularly prominent in Internet of Things (IoT) and real-time systems applications, which interface with hardware devices that come with inherent timing constraints. Verifying compliance of such systems with the intended\n                    <jats:italic toggle=\"yes\">timed protocol<\/jats:italic>\n                    is challenged by their\n                    <jats:italic toggle=\"yes\">heterogeneity<\/jats:italic>\n                    \u2014ruling out any verification method that relies on the system to be implemented in one common language, let alone in a high-level and typed programming language. To address this challenge, this paper contributes a\n                    <jats:italic toggle=\"yes\">logical relation<\/jats:italic>\n                    to verify that its inhabitants (the applications and hardware devices to be proved correct) comply with the given timed protocol. To cater to the systems\u2019 heterogeneity, the logical relation is entirely\n                    <jats:italic toggle=\"yes\">semantic<\/jats:italic>\n                    , lifting the requirement that its inhabitants are syntactically well-typed. A semantic approach enables two modes of use of the logical relation for program verification:\n                    <jats:italic toggle=\"yes\">(i) once-and-for-all<\/jats:italic>\n                    verification of an\n                    <jats:italic toggle=\"yes\">arbitrary<\/jats:italic>\n                    well-typed application, given a type system, and\n                    <jats:italic toggle=\"yes\">(ii) per-instance<\/jats:italic>\n                    verification of a specific application \/ hardware device (\n                    <jats:italic toggle=\"yes\">a.k.a<\/jats:italic>\n                    ., foreign code). To facilitate mode\n                    <jats:italic toggle=\"yes\">(i)<\/jats:italic>\n                    , the paper develops a refinement type system for expressing timed message-passing protocols and proves that any well-typed program inhabits the logical relation (fundamental theorem). A type checker for the refinement type system has been implemented in Rust, using an SMT solver to check satisfiability of timing constraints. Then, the paper demonstrates both modes of use based on a small case study of a smart home system for monitoring air quality, consisting of a controller application and various environment sensors.\n                  <\/jats:p>","DOI":"10.1145\/3704895","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"1750-1781","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Semantic Logical Relations for Timed Message-Passing Protocols"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8523-5156","authenticated-orcid":false,"given":"Yue","family":"Yao","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-4138-5001","authenticated-orcid":false,"given":"Grant","family":"Iraci","sequence":"additional","affiliation":[{"name":"University at Buffalo, Buffalo, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3961-7118","authenticated-orcid":false,"given":"Cheng-En","family":"Chuang","sequence":"additional","affiliation":[{"name":"University at Buffalo, Buffalo, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8347-3529","authenticated-orcid":false,"given":"Stephanie","family":"Balzer","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4353-1998","authenticated-orcid":false,"given":"Lukasz","family":"Ziarek","sequence":"additional","affiliation":[{"name":"University at Buffalo, Buffalo, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2309.00192"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-13(4:25)2017"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0020949"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","unstructured":"Nick Benton and Chung-Kil Hur. 2009. Biorthogonality Step-Indexing and Compiler Correctness. In 14th ACM SIGPLAN International Conference on Functional Programming (ICFP). ACM 97\u2013108. https:\/\/doi.org\/10.1145\/1596550.1596567 10.1145\/1596550.1596567","DOI":"10.1145\/1596550.1596567"},{"key":"e_1_3_2_8_1","unstructured":"G\u00e9rard Berry. 1999. The Constructive Semantics of Pure Esterel. Technical Report. \u00c9cole des Mines de Paris and INRIA."},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(92)90005-V"},{"key":"e_1_3_2_10_1","unstructured":"Bluetooth SIG 2023. Bluetooth Core Specification. Bluetooth SIG. 5.4."},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_21"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44584-6_29"},{"key":"e_1_3_2_13_1","unstructured":"Bosch. 2024. Gas Sensor BME680. https:\/\/www.bosch-sensortec.com\/products\/environmental-sensors\/gas-sensors\/bme680\/."},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30044-8_14"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_19"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_16"},{"key":"e_1_3_2_17_1","unstructured":"Mauricio Cano Ilaria Castellani Cinzia Di Giusto and Jorge A. P\u00e9rez . 2019. Multiparty Reactive Sessions. Technical Report 9270. INRIA."},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2022.22"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250742"},{"key":"e_1_3_2_20_1","unstructured":"Robert L. Constable Stuart F. Allen Mark Bromley Rance Cleaveland J. F. Cremer Robert Harper Douglas J. Howe Todd B. Knoblock Nax Paul Mendler Prakash Panangaden James T. Sasaki and Scott F. Smith. 1986. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall. http:\/\/dl.acm.org\/citation.cfm?id=10510"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236786"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209146"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICRCC.2012.6450552"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3610612.3610621"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470654"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2024.11"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.46298\/LMCS-18(2:8)2022"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2020.29"},{"key":"e_1_3_2_29_1","unstructured":"Jean-Yves Girard. 1972. Interpr\u00e9tation fonctionelle et \u00e9limination des coupures de l'arithm\u00e9tique d'ordre sup\u00e9rieur. Ph. D. Dissertation. Universit\u00e9 Paris VII."},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.97300"},{"key":"e_1_3_2_31_1","volume-title":"First-Order Dynamic Logic","year":"1979","unstructured":"David Harel. 1979. First-Order Dynamic Logic. Springer-Verlag, Berlin, Heidelberg."},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57208-2_35"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19056-8_4"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053567"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328472"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360215"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622854"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2808098.2808100"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1620405.1620412"},{"key":"e_1_3_2_42_1","doi-asserted-by":"crossref","unstructured":"J. Klensin. 2001. RFC2821: Simple Mail Transfer Protocol.","DOI":"10.17487\/rfc2821"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1997.614941"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.IC.2010.09.008"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290337"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01995674"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_24"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","unstructured":"Kai Lampka Simon Perathoner and Lothar Thiele. 2009. Analytic real-time analysis and timed automata: a hybrid method for analyzing embedded real-time systems. In 9th ACM & IEEE International conference on Embedded software (EMSOFT). ACM 107\u2013116. https:\/\/doi.org\/10.1145\/1629335.1629351 10.1145\/1629335.1629351","DOI":"10.1145\/1629335.1629351"},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_23"},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951921"},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","unstructured":"Robin Milner. 1980. A Calculus of Communicating Systems. Lecture Notes in Computer Science Vol.92. Springer. https:\/\/doi.org\/10.1007\/3-540-10235-3 10.1007\/3-540-10235-3","DOI":"10.1007\/3-540-10235-3"},{"key":"e_1_3_2_53_1","volume-title":"Communicating and Mobile Systems: the n-calculus.","author":"Milner Robin","year":"1999","unstructured":"Robin Milner. 1999. Communicating and Mobile Systems: the n-calculus. Cambridge University Press."},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237791"},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/S00165-017-0420-8"},{"key":"e_1_3_2_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.33"},{"key":"e_1_3_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523703"},{"key":"e_1_3_2_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_27"},{"key":"e_1_3_2_59_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.08.001"},{"key":"e_1_3_2_60_1","first-page":"227","article-title":"Operational Reasoning for Functions with Local State","author":"Pitts Andrew M.","year":"1998","unstructured":"Andrew M. Pitts and Ian Stark. 1998. Operational Reasoning for Functions with Local State. Higher Order Operational Techniques in Semantics (HOOTS) (1998), 227\u2013273.","journal-title":"Higher Order Operational Techniques in Semantics (HOOTS)"},{"key":"e_1_3_2_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9103-8"},{"key":"e_1_3_2_62_1","unstructured":"Gordon D. Plotkin. 1973. Lambda-definability and logical relations. Technical Report. University of Edinburgh."},{"key":"e_1_3_2_63_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_2_64_1","volume-title":"The n-calculus: a Theory of Mobile Processes.","year":"2001","unstructured":"Davide Sangiorgi and David Walker. 2001. The n-calculus: a Theory of Mobile Processes. Cambridge University Press."},{"key":"e_1_3_2_65_1","unstructured":"NXP Semiconductors. 2021. I2C-bus specification and user manual. Stand ard. NXP Semiconductors."},{"key":"e_1_3_2_66_1","unstructured":"SEP. 1999. Stanford Encyclopedia of Philosophy: Temporal Logic. https:\/\/plato.stanford.edu\/entries\/logic-temporal\/."},{"key":"e_1_3_2_67_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(85)80001-2"},{"key":"e_1_3_2_68_1","doi-asserted-by":"publisher","DOI":"10.2307\/2271658"},{"key":"e_1_3_2_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/3676954"},{"key":"e_1_3_2_70_1","unstructured":"Bernardo Toninho. 2015. A Logical Foundation for Session-Based Concurrent Computation. Ph. D. Dissertation. Carnegie Mellon University and New University of Lisbon."},{"key":"e_1_3_2_71_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_20"},{"key":"e_1_3_2_72_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2024.40"},{"key":"e_1_3_2_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364568"},{"key":"e_1_3_2_74_1","doi-asserted-by":"publisher","DOI":"10.13154\/tches.v2019.i3.66-85"},{"key":"e_1_3_2_75_1","doi-asserted-by":"publisher","unstructured":"Yue Yao Grant Iraci Cheng-En Chuang Stephanie Balzer and Lukasz Ziarek. 2024a. Semantic Logical Relations for Timed Message- Passing Protocols (Artifact). https:\/\/doi.org\/10.5281\/zenodo.13937290 10.5281\/zenodo.13937290","DOI":"10.5281\/zenodo.13937290"},{"key":"e_1_3_2_76_1","unstructured":"Yue Yao Grant Iraci Cheng-En Chuang Stephanie Balzer and Lukasz Ziarek. 2024b. Semantic Logical Relations for Timed Message-Passing Protocols (Extended Version). arXiv:2411.07215 [cs.PL] https:\/\/arxiv.org\/abs\/2411.07215"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704895","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704895","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:15:41Z","timestamp":1770200141000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704895"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":75,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704895"],"URL":"https:\/\/doi.org\/10.1145\/3704895","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}