{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T23:10:30Z","timestamp":1765667430220,"version":"3.40.3"},"publisher-location":"Cham","reference-count":14,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031213137"},{"type":"electronic","value":"9783031213144"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"vor","delay-in-days":365,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Task-oriented programming (<jats:sc>top<\/jats:sc>) is a new programming paradigm for specifying multi-user workflows. To reason formally about<jats:sc>top<\/jats:sc>programs, a formal language called<jats:sc>TopHat<\/jats:sc>has been designed, together with its operational semantics. For proving properties about task-oriented programs, it is desirable to know when two<jats:sc>TopHat<\/jats:sc>-programs are semantically equivalent. This paper aims to answer this question. We show that a task can be in either one of five conditions, and for every two tasks in the same condition, we define what it means for them to be semantically equivalent. Using this definition, we study a number of transformation laws for<jats:sc>TopHat<\/jats:sc>-programs, which can be used by developers and compilers to optimise<jats:sc>top<\/jats:sc>-programs. We show that the \"Image missing\"operation on types in<jats:sc>TopHat<\/jats:sc>is a functor but cannot be a monad. We support our findings with proofs formalised in the dependently typed programming language<jats:sc>Idris<\/jats:sc>.<\/jats:p>","DOI":"10.1007\/978-3-031-21314-4_6","type":"book-chapter","created":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T05:12:32Z","timestamp":1672549952000},"page":"100-125","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Semantic Equivalence of Task-Oriented Programs in TopHat"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0982-5880","authenticated-orcid":false,"given":"Tosca","family":"Klijnsma","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8436-2054","authenticated-orcid":false,"given":"Tim","family":"Steenvoorden","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,1,1]]},"reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-319-15940-9_5","volume-title":"Central European Functional Programming School","author":"P Achten","year":"2015","unstructured":"Achten, P., Koopman, P., Plasmeijer, R.: An introduction to task oriented programming. In: Zs\u00f3k, V., Horv\u00e1th, Z., Csat\u00f3, L. (eds.) CEFP 2013. LNCS, vol. 8606, pp. 187\u2013245. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-15940-9_5"},{"issue":"5","key":"6_CR2","doi-asserted-by":"publisher","first-page":"552","DOI":"10.1017\/S095679681300018X","volume":"23","author":"EC Brady","year":"2013","unstructured":"Brady, E.C.: Idris, a general-purpose dependently typed programming language: design and implementation. J. Funct. Program. 23(5), 552\u2013593 (2013)","journal-title":"J. Funct. Program."},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/978-3-642-24452-0_12","volume-title":"Implementation and Application of Functional Languages","author":"P Koopman","year":"2011","unstructured":"Koopman, P., Plasmeijer, R., Achten, P.: An executable and testable semantics for iTasks. In: Scholz, S.-B., Chitil, O. (eds.) IFL 2008. LNCS, vol. 5836, pp. 212\u2013232. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24452-0_12"},{"key":"6_CR4","unstructured":"Lijnse, B., Jansen, J.M., Plasmeijer, R.: Incidone: a task-oriented incident coordination tool. In: Proceedings of ISCRAM (2012)"},{"issue":"1","key":"6_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1017\/S0956796807006326","volume":"18","author":"C McBride","year":"2008","unstructured":"McBride, C., Paterson, R.: Applicative programming with effects. J. Funct. Program. 18(1), 1\u201313 (2008)","journal-title":"J. Funct. Program."},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-030-57761-2_3","volume-title":"Trends in Functional Programming","author":"N Naus","year":"2020","unstructured":"Naus, N., Steenvoorden, T.: Generating next step hints for task oriented programs using symbolic execution. In: Byrski, A., Hughes, J. (eds.) TFP 2020. LNCS, vol. 12222, pp. 47\u201368. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-57761-2_3"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Naus, N., Steenvoorden, T., Klinik, M.: A symbolic execution semantics for TopHat. In: Stutterheim, J., Chin, W. (eds.) IFL 2019: Implementation and Application of Functional Languages, Singapore, 25\u201327 September 2019, pp. 1:1\u20131:11. ACM (2019)","DOI":"10.1145\/3412932.3412933"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/3-540-45699-6_8","volume-title":"Applied Semantics","author":"AM Pitts","year":"2002","unstructured":"Pitts, A.M.: Operational semantics and program equivalence. In: Barthe, G., Dybjer, P., Pinto, L., Saraiva, J. (eds.) APPSEM 2000. LNCS, vol. 2395, pp. 378\u2013412. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45699-6_8"},{"key":"6_CR9","unstructured":"Plasmeijer, R., van Eekelen, M., van Groningen, J.: Clean language report version 2.1. Technical report. Radboud University, Nijmegen, The Netherlands (2002)"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Plasmeijer, R., Lijnse, B., Michels, S., Achten, P., Koopman, P.W.M.: Task-oriented programming in a pure functional language. In: Schreye, D.D., Janssens, G., King, A. (eds.) Principles and Practice of Declarative Programming, PPDP 2012, Leuven, Belgium, 19\u201321 September 2012, pp. 195\u2013206. ACM (2012)","DOI":"10.1145\/2370776.2370801"},{"key":"6_CR11","unstructured":"Sewell, P.: Semantics of programming languages, computer science Tripos, part 1B (2017). Accessed 29 Nov 2019"},{"key":"6_CR12","unstructured":"Steenvoorden, T.: TopHat: task-oriented programming with style. Ph.D. thesis. Radboud University, Nijmegen, The Netherlands (2022)"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"Steenvoorden, T., Naus, N., Klinik, M.: TopHat: a formal foundation for task-oriented programming. In: Komendantskaya, E. (ed.) Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages, PPDP 2019, Porto, Portugal, 7\u20139 October 2019, pp. 17:1\u201317:13. ACM (2019)","DOI":"10.1145\/3354166.3354182"},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-319-89719-6_2","volume-title":"Trends in Functional Programming","author":"J Stutterheim","year":"2018","unstructured":"Stutterheim, J., Achten, P., Plasmeijer, R.: Maintaining separation of concerns through task oriented software development. In: Wang, M., Owens, S. (eds.) TFP 2017. LNCS, vol. 10788, pp. 19\u201338. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89719-6_2"}],"container-title":["Lecture Notes in Computer Science","Trends in Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-21314-4_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,11]],"date-time":"2024-10-11T10:26:58Z","timestamp":1728642418000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-21314-4_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031213137","9783031213144"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-21314-4_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"1 January 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TFP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Trends in Functional Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 March 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 March 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tfp2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/trendsfp.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"17","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"53% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}