{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T16:12:10Z","timestamp":1784304730743,"version":"3.55.0"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2019,7,26]],"date-time":"2019-07-26T00:00:00Z","timestamp":1564099200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100008398","name":"VILLUM FONDEN","doi-asserted-by":"crossref","award":["13156"],"award-info":[{"award-number":["13156"]}],"id":[{"id":"10.13039\/100008398","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,7,26]]},"abstract":"<jats:p>Functional reactive programming (FRP) is a paradigm for programming with signals and events, allowing the user to describe reactive programs on a high level of abstraction. For this to make sense, an FRP language must ensure that all programs are causal, and can be implemented without introducing space leaks and time leaks. To this end, some FRP languages do not give direct access to signals, but just to signal functions.<\/jats:p>\n          <jats:p>\n            Recently, modal types have been suggested as an alternative approach to ensuring causality in FRP languages in the synchronous case, giving direct access to the signal and event abstractions. This paper presents\n            <jats:italic>Simply RaTT<\/jats:italic>\n            , a new modal calculus for reactive programming. Unlike prior calculi, Simply RaTT uses a Fitch-style approach to modal types, which simplifies the type system and makes programs more concise. Echoing a previous result by Krishnaswami for a different language, we devise an operational semantics that safely executes Simply RaTT programs without space leaks.\n          <\/jats:p>\n          <jats:p>We also identify a source of time leaks present in other modal FRP languages: The unfolding of fixed points in delayed computations. The Fitch-style presentation allows an easy way to rules out these leaks, which appears not to be possible in the more traditional dual context approach.<\/jats:p>","DOI":"10.1145\/3341713","type":"journal-article","created":{"date-parts":[[2019,7,29]],"date-time":"2019-07-29T20:55:51Z","timestamp":1564433751000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Simply RaTT: a fitch-style modal calculus for reactive programming without space leaks"],"prefix":"10.1145","volume":"3","author":[{"given":"Patrick","family":"Bahr","sequence":"first","affiliation":[{"name":"IT University of Copenhagen, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christian Uldal","family":"Graulund","sequence":"additional","affiliation":[{"name":"IT University of Copenhagen, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rasmus Ejlers","family":"M\u00f8gelberg","sequence":"additional","affiliation":[{"name":"IT University of Copenhagen, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,7,26]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/3329995.3330032"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.16"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/41625.41641"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535881"},{"key":"e_1_2_2_7_1","volume-title":"Foundations of Software Science and Computation Structures","author":"Clouston Ranald"},{"key":"e_1_2_2_8_1","volume-title":"Andrew M. Pitts, and Bas Spitters.","author":"Clouston Ranald","year":"2018"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/258948.258973"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596638.1596643"},{"key":"e_1_2_2_11_1","unstructured":"Pascal Raymond Erwan Jahier and Nicolas Halbwachs. 2019. The LUSTRE V6 Reference Manual. https:\/\/www- verimag. imag.fr\/DIST- TOOLS\/SYNCHRONE\/lustre- v6\/doc\/lv6- ref- man.pdf  Pascal Raymond Erwan Jahier and Nicolas Halbwachs. 2019. The LUSTRE V6 Reference Manual. https:\/\/www- verimag. imag.fr\/DIST- TOOLS\/SYNCHRONE\/lustre- v6\/doc\/lv6- ref- man.pdf"},{"key":"e_1_2_2_12_1","unstructured":"Esterel Technologies SA. 2019a. Scientific Background. http:\/\/www.esterel- technologies.com\/about- us\/scientific- historicbackground\/ .  Esterel Technologies SA. 2019a. Scientific Background. http:\/\/www.esterel- technologies.com\/about- us\/scientific- historicbackground\/ ."},{"key":"e_1_2_2_13_1","unstructured":"Esterel Technologies SA. 2019b. Success Stories. http:\/\/www.esterel- technologies.com\/success- stories\/ .  Esterel Technologies SA. 2019b. Success Stories. http:\/\/www.esterel- technologies.com\/success- stories\/ ."},{"key":"e_1_2_2_14_1","volume-title":"Symbolic logic, an introduction","author":"Fitch Frederic Benton"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209148"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103776.2103783"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603106"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2428116.2428128"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500588"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.38"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103665"},{"key":"e_1_2_2_22_1","volume-title":"The Clocks They Are Adjunctions: Denotational Semantics for Clocked Type Theory. In 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018","volume":"108","author":"Mannaa Bassel","year":"2018"},{"key":"e_1_2_2_23_1","doi-asserted-by":"crossref","volume-title":"Intuitionistic type theory","author":"Martin-L\u00f6f Per","DOI":"10.1093\/oso\/9780198501275.003.0010"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006326"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/788022.789002"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/581690.581695"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_2_28_1","first-page":"25","article-title":"Lucid synchrone, version 3. Tutorial and reference manual. Universit\u00e9 Paris-Sud","volume":"1","author":"Pouzet Marc","year":"2006","journal-title":"LRI"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341713","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341713","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:43:24Z","timestamp":1750207404000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341713"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,26]]},"references-count":27,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2019,7,26]]}},"alternative-id":["10.1145\/3341713"],"URL":"https:\/\/doi.org\/10.1145\/3341713","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,7,26]]},"assertion":[{"value":"2019-07-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}