{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:55Z","timestamp":1779836755131,"version":"3.53.1"},"reference-count":64,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2020,5,7]],"date-time":"2020-05-07T00:00:00Z","timestamp":1588809600000},"content-version":"unspecified","delay-in-days":127,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Highly critical application domains, like medicine and aerospace, require the use of strict design, implementation, and validation techniques. Functional languages have been used in these domains to develop synchronous dataflow programming languages for reactive systems. Causal stream functions and functional reactive programming (FRP) capture the essence of those languages in a way that is both elegant and robust. To guarantee that critical systems can operate under high stress over long periods of time, these applications require clear specifications of possible faults and hazards, and how they are being handled. Modeling failure is straightforward in functional languages, and many functional reactive abstractions incorporate support for failure or termination. However, handling\n                    <jats:italic>unknown types of faults<\/jats:italic>\n                    , and incorporating\n                    <jats:italic>fault tolerance<\/jats:italic>\n                    into FRP, requires a different construction and remains an open problem. This work demonstrates how to extend an existing functional reactive framework with fault tolerance features. At value level, we tag faulty signals with reliability and probability information and use random testing to inject faults and validate system properties encoded in temporal logic. At type level, we tag components with the kinds of faults they may exhibit and use type-level programming to obtain compile-time guarantees of key aspects of fault tolerance. Our approach is powerful enough to be used in systems with realistic complexity, and flexible enough to be used to guide system analysis and design, validate system properties in the presence of faults, perform runtime monitoring, and study the effects of different fault tolerance mechanisms.\n                  <\/jats:p>","DOI":"10.1017\/s0956796820000118","type":"journal-article","created":{"date-parts":[[2020,5,7]],"date-time":"2020-05-07T03:44:57Z","timestamp":1588823097000},"source":"Crossref","is-referenced-by-count":6,"title":["Fault-tolerant functional reactive programming (extended version)"],"prefix":"10.1017","volume":"30","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9998-0269","authenticated-orcid":false,"given":"IVAN","family":"PEREZ","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"ALWYN E.","family":"GOODLOE","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2020,5,7]]},"reference":[{"key":"S0956796820000118_ref61","first-page":"103","article-title":"Towards runtime system level fault tolerance for a distributed functional language","volume":"2","author":"Trinder","year":"2000","journal-title":"Trends Func. Program."},{"key":"S0956796820000118_ref60","article-title":"Transparent fault tolerance for scalable functional computation","volume":"26","author":"Stewart","year":"2016","journal-title":"J. Func. Program."},{"key":"S0956796820000118_ref58","unstructured":"Stewart, R. (2013) Reliable Massively Parallel Symbolic Computing: Fault Tolerance for a Distributed Haskell. Ph.D. thesis, Heriot-Watt University."},{"key":"S0956796820000118_ref55","unstructured":"RTCA. (2011) Software Considerations in Airborne Systems and Equipment Certification (178C). Technical report."},{"key":"S0956796820000118_ref54","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29860-8_23"},{"key":"S0956796820000118_ref53","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16612-9_26"},{"key":"S0956796820000118_ref52","unstructured":"Pfeifer, H. , Schwier, D. & Von Henke, F. W. (1999) Formal verification for time-triggered clock synchronization. Depend. Comput. Crit. Appl. 7, 207\u2013226."},{"key":"S0956796820000118_ref51","doi-asserted-by":"publisher","DOI":"10.1109\/SMC-IT.2019.00011"},{"key":"S0956796820000118_ref62","article-title":"Reliability with Erlang","volume":"11","author":"Vinoski","year":"2007","journal-title":"IEEE Internet Comput"},{"key":"S0956796820000118_ref57","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(90)90056-J"},{"key":"S0956796820000118_ref49","unstructured":"Perez, I. & Nilsson, H. Runtime verification and validation of functional reactive systems. J. Func. Program. Submitted (Under evaluation)."},{"key":"S0956796820000118_ref48","doi-asserted-by":"publisher","DOI":"10.1145\/3110246"},{"key":"S0956796820000118_ref50","doi-asserted-by":"publisher","DOI":"10.1145\/2976002.2976010"},{"key":"S0956796820000118_ref47","doi-asserted-by":"publisher","DOI":"10.1145\/3236791"},{"key":"S0956796820000118_ref22","doi-asserted-by":"publisher","DOI":"10.1145\/258949.258973"},{"key":"S0956796820000118_ref13","unstructured":"Butler, R. W. (1996) An Introduction to Requirements Capture Using PVS: Specification of a Simple Autopilot. Technical report."},{"key":"S0956796820000118_ref20","unstructured":"Driscoll, K. (2008) Real system failures. https:\/\/c3.nasa.gov\/dashlink\/static\/media\/other\/ObservedFailures4.html"},{"key":"S0956796820000118_ref19","unstructured":"Dormoy, F.-X. (2008) Scade 6: A model based solution for safety critical software development. Proceedings of the 4th European Congress on Embedded Real Time Software (ERTS 2008), pp. 1\u20139."},{"key":"S0956796820000118_ref32","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511805318"},{"key":"S0956796820000118_ref14","doi-asserted-by":"publisher","DOI":"10.1145\/871895.871897"},{"key":"S0956796820000118_ref12","doi-asserted-by":"publisher","DOI":"10.1109\/32.210303"},{"key":"S0956796820000118_ref38","doi-asserted-by":"publisher","DOI":"10.1145\/581690.581695"},{"key":"S0956796820000118_ref11","unstructured":"Butler, R. W. (2008, February). A Primer on Architectural Level Fault Tolerance. Technical report. NASA\/TM-2008-215108, L-19403. NASA Langley Research Center."},{"key":"S0956796820000118_ref63","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-15975-4_33"},{"key":"S0956796820000118_ref59","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40447-4_16"},{"key":"S0956796820000118_ref23","doi-asserted-by":"publisher","DOI":"10.1145\/2096148.2034690"},{"key":"S0956796820000118_ref42","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55602-8_217"},{"key":"S0956796820000118_ref56","unstructured":"Rushby, J. (2006) PVS Bibliography. http:\/\/pvs.csl.sri.com\/documentation.shtml"},{"key":"S0956796820000118_ref1","doi-asserted-by":"publisher","DOI":"10.1145\/1465611.1465708"},{"key":"S0956796820000118_ref18","unstructured":"Di Vito, B. L. & Roberts, L. W. (1996) Using Formal Methods to Assist in the Requirements Analysis of the Space Shuttle GPS Change Request. Technical report."},{"key":"S0956796820000118_ref6","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(99)00015-5"},{"key":"S0956796820000118_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60973-3_86"},{"key":"S0956796820000118_ref30","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"S0956796820000118_ref2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1976.1674598"},{"key":"S0956796820000118_ref3","doi-asserted-by":"publisher","DOI":"10.1145\/3242744.3242757"},{"key":"S0956796820000118_ref46","doi-asserted-by":"publisher","DOI":"10.1145\/3122955.3122957"},{"key":"S0956796820000118_ref10","doi-asserted-by":"publisher","DOI":"10.1145\/2544174.2500581"},{"key":"S0956796820000118_ref7","doi-asserted-by":"publisher","DOI":"10.1109\/5.97299"},{"key":"S0956796820000118_ref35","doi-asserted-by":"publisher","DOI":"10.1109\/FTCS.1993.627343"},{"key":"S0956796820000118_ref64","doi-asserted-by":"publisher","DOI":"10.1109\/HPCC-SmartCity-DSS.2016.0104"},{"key":"S0956796820000118_ref36","doi-asserted-by":"publisher","DOI":"10.1109\/CMPASS.1994.318462"},{"key":"S0956796820000118_ref8","doi-asserted-by":"publisher","DOI":"10.1145\/2897336.2897340"},{"key":"S0956796820000118_ref27","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(99)00023-4"},{"key":"S0956796820000118_ref31","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"key":"S0956796820000118_ref9","doi-asserted-by":"publisher","DOI":"10.1145\/2976002.2976012"},{"key":"S0956796820000118_ref24","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796805005721"},{"key":"S0956796820000118_ref28","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535846"},{"key":"S0956796820000118_ref5","unstructured":"Bedingfield, K. , Leach, R. D. & Alexander, M. B. (1996, August) Spacecraft System Failures and Anomalies Attributed to the Natural Space Environment. Technical report, National Aeronautics and Space Administration. NASA Reference Publication 1390."},{"key":"S0956796820000118_ref25","doi-asserted-by":"publisher","DOI":"10.1109\/5.97300"},{"key":"S0956796820000118_ref26","first-page":"107","volume-title":"Symposium on Implementation and Application of Functional Languages","author":"Huch","year":"2000"},{"key":"S0956796820000118_ref33","doi-asserted-by":"publisher","DOI":"10.1145\/357172.357176"},{"key":"S0956796820000118_ref29","doi-asserted-by":"publisher","DOI":"10.1145\/2578854.2503791"},{"key":"S0956796820000118_ref40","doi-asserted-by":"publisher","DOI":"10.1145\/2775050.2633368"},{"key":"S0956796820000118_ref34","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199528"},{"key":"S0956796820000118_ref44","unstructured":"Owre, S. , Shankar, N. , Rushby, J. M. & Stringer-Calvert, D. W. J. (1999) PVS Language Reference. Technical report."},{"key":"S0956796820000118_ref4","unstructured":"B\u00e4renz, M. , Perez, I. & Nilsson, H. (2016) Mathematical properties of monadic stream functions. Available at: http:\/\/cs.nott.ac.uk\/~ixp\/papers\/msfmathprops.pdf"},{"key":"S0956796820000118_ref37","doi-asserted-by":"publisher","DOI":"10.1145\/2633357.2633363"},{"key":"S0956796820000118_ref15","doi-asserted-by":"publisher","DOI":"10.1145\/287000.287023"},{"key":"S0956796820000118_ref39","doi-asserted-by":"publisher","DOI":"10.1145\/2633357.2633368"},{"key":"S0956796820000118_ref41","unstructured":"Orchard, D. A. , Petricek, T. & Mycroft, A. (2014) The semantic marriage of monads and effects. CoRR, abs\/1401.5391."},{"key":"S0956796820000118_ref17","doi-asserted-by":"publisher","DOI":"10.1109\/DCFTS.1999.814300"},{"key":"S0956796820000118_ref43","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61474-5_91"},{"key":"S0956796820000118_ref21","doi-asserted-by":"publisher","DOI":"10.1109\/32.588520"},{"key":"S0956796820000118_ref45","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596582"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796820000118","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:51Z","timestamp":1779835011000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796820000118\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"references-count":64,"alternative-id":["S0956796820000118"],"URL":"https:\/\/doi.org\/10.1017\/s0956796820000118","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"article-number":"e12"}}