{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,28]],"date-time":"2025-11-28T17:23:25Z","timestamp":1764350605305,"version":"3.40.3"},"publisher-location":"Cham","reference-count":46,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030613617"},{"type":"electronic","value":"9783030613624"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-61362-4_28","type":"book-chapter","created":{"date-parts":[[2020,10,28]],"date-time":"2020-10-28T13:02:36Z","timestamp":1603890156000},"page":"489-508","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Safe Sessions of Channel Actions in Clojure: A Tour of the Discourje Project"],"prefix":"10.1007","author":[{"given":"Ruben","family":"Hamers","sequence":"first","affiliation":[]},{"given":"Sung-Shik","family":"Jongmans","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,10,29]]},"reference":[{"issue":"2\u20133","key":"28_CR1","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1561\/2500000031","volume":"3","author":"D Ancona","year":"2016","unstructured":"Ancona, D., et al.: Behavioral types in programming languages. Found. Trends Program. Lang. 3(2\u20133), 95\u2013230 (2016)","journal-title":"Found. Trends Program. Lang."},{"key":"28_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11804192_17"},{"key":"28_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-75632-5_1","volume-title":"Lectures on Runtime Verification","author":"E Bartocci","year":"2018","unstructured":"Bartocci, E., Falcone, Y., Francalanza, A., Reger, G.: Introduction to runtime verification. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 1\u201333. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-75632-5_1"},{"key":"28_CR4","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1016\/j.tcs.2017.02.009","volume":"669","author":"L Bocchi","year":"2017","unstructured":"Bocchi, L., Chen, T., Demangeon, R., Honda, K., Yoshida, N.: Monitoring networks through multiparty session types. Theor. Comput. Sci. 669, 33\u201358 (2017)","journal-title":"Theor. Comput. Sci."},{"key":"28_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-642-15375-4_12","volume-title":"CONCUR 2010 - Concurrency Theory","author":"L Bocchi","year":"2010","unstructured":"Bocchi, L., Honda, K., Tuosto, E., Yoshida, N.: A theory of design-by-contract for distributed multiparty interactions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 162\u2013176. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-15375-4_12"},{"key":"28_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-662-49498-1_4","volume-title":"Programming Languages and Systems","author":"A Bonnaire-Sergeant","year":"2016","unstructured":"Bonnaire-Sergeant, A., Davies, R., Tobin-Hochstadt, S.: Practical optional types for Clojure. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 68\u201394. Springer, Heidelberg (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-662-49498-1_4"},{"doi-asserted-by":"crossref","unstructured":"Castro, D., Hu, R., Jongmans, S., Ng, N., Yoshida, N.: Distributed programming using role-parametric session types in go: statically-typed endpoint APIs for dynamically-instantiated communication structures. PACMPL 3(POPL), 29:1\u201329:30 (2019)","key":"28_CR7","DOI":"10.1145\/3290342"},{"unstructured":"Clojure Team: Clojure - Clojure core.async Channels, 28 June 2013. \nhttps:\/\/clojure.org\/news\/2013\/06\/28\/clojure-clore-async-channels\n\n. Accessed 1 Sept 2019","key":"28_CR8"},{"unstructured":"Clojure Team: Clojure - State of Clojure 2019 Results, 04 February 2019. \nhttps:\/\/clojure.org\/news\/2019\/02\/04\/state-of-clojure-2019\n\n. Accessed 1 Sept 2019","key":"28_CR9"},{"unstructured":"Clojure Team: Clojure - State of Clojure 2020 Results, 20 February 2019. \nhttps:\/\/clojure.org\/news\/2020\/02\/20\/state-of-clojure-2020\n\n. Accessed 28 May 2020","key":"28_CR10"},{"unstructured":"Clojure Team: Clojure (nd). \nhttps:\/\/clojure.org\n\n. Accessed 1 Sept 2019","key":"28_CR11"},{"key":"28_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E Cohen","year":"2009","unstructured":"Cohen, E., et al.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23\u201342. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-03359-9_2"},{"issue":"3","key":"28_CR13","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/s10703-014-0218-8","volume":"46","author":"R Demangeon","year":"2015","unstructured":"Demangeon, R., Honda, K., Hu, R., Neykova, R., Yoshida, N.: Practical interruptible conversations: distributed dynamic verification with multiparty session types and python. Formal Methods Syst. Des. 46(3), 197\u2013225 (2015)","journal-title":"Formal Methods Syst. Des."},{"key":"28_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3\u2014where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-37036-6_8"},{"key":"28_CR15","series-title":"Texts in Theoretical Computer Science. An EATCS Series","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-04293-9","volume-title":"Introduction to Process Algebra","author":"W Fokkink","year":"2000","unstructured":"Fokkink, W.: Introduction to Process Algebra. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2000). \nhttps:\/\/doi.org\/10.1007\/978-3-662-04293-9"},{"unstructured":"Go Team: Go 2016 Survey Results - The Go Blog, 03 June 2017. \nhttps:\/\/blog.golang.org\/survey2016-results\n\n. Accessed 1 Sept 2019","key":"28_CR16"},{"unstructured":"Go Team: Go 2017 Survey Results - The Go Blog, 26 February 2018. \nhttps:\/\/blog.golang.org\/survey2017-results\n\n. Accessed 1 Sept 2019","key":"28_CR17"},{"unstructured":"Go Team: Go 2018 Survey Results - The Go Blog, 28 March 2019. \nhttps:\/\/blog.golang.org\/survey2018-results\n\n. Accessed 1 Sept 2019","key":"28_CR18"},{"unstructured":"Go Team: Go Developer Survey 2019 Results - The Go Blog, 20 April 2020. \nhttps:\/\/blog.golang.org\/survey2019-results\n\n. Accessed 8 May 2020","key":"28_CR19"},{"unstructured":"Go Team: Effective Go - The Go Programming Language (nd). \nhttps:\/\/golang.org\/doc\/effective_go.html\n\n. Accessed 8 May 2020","key":"28_CR20"},{"unstructured":"Go Team: The Go Programming Language (nd). \nhttps:\/\/golang.org\n\n. Accessed 1 Sept 2019","key":"28_CR21"},{"key":"28_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-030-45190-5_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Hamers","year":"2020","unstructured":"Hamers, R., Jongmans, S.-S.: Discourje: runtime verification of communication protocols in Clojure. In: Biere, A., Parker, D. (eds.) TACAS 2020. LNCS, vol. 12078, pp. 266\u2013284. Springer, Cham (2020). \nhttps:\/\/doi.org\/10.1007\/978-3-030-45190-5_15"},{"doi-asserted-by":"crossref","unstructured":"Hickey, R.: The Clojure programming language. In: DLS, p. 1. ACM (2008)","key":"28_CR23","DOI":"10.1145\/1408681.1408682"},{"doi-asserted-by":"crossref","unstructured":"Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: POPL, pp. 273\u2013284. ACM (2008)","key":"28_CR24","DOI":"10.1145\/1328897.1328472"},{"key":"28_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-642-40787-1_8","volume-title":"Runtime Verification","author":"R Hu","year":"2013","unstructured":"Hu, R., Neykova, R., Yoshida, N., Demangeon, R., Honda, K.: Practical interruptible conversations. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 130\u2013148. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-40787-1_8"},{"key":"28_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-662-49665-7_24","volume-title":"Fundamental Approaches to Software Engineering","author":"R Hu","year":"2016","unstructured":"Hu, R., Yoshida, N.: Hybrid session verification through endpoint API generation. In: Stevens, P., W\u0105sowski, A. (eds.) FASE 2016. LNCS, vol. 9633, pp. 401\u2013418. Springer, Heidelberg (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-662-49665-7_24"},{"key":"28_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-662-54494-5_7","volume-title":"Fundamental Approaches to Software Engineering","author":"R Hu","year":"2017","unstructured":"Hu, R., Yoshida, N.: Explicit connection actions in multiparty session types. In: Huisman, M., Rubin, J. (eds.) FASE 2017. LNCS, vol. 10202, pp. 116\u2013133. Springer, Heidelberg (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-662-54494-5_7"},{"doi-asserted-by":"crossref","unstructured":"H\u00fcttel, H., et al.: Foundations of session types and behavioural contracts. ACM Comput. Surv. 49(1), 3:1\u20133:36 (2016)","key":"28_CR28","DOI":"10.1145\/2873052"},{"key":"28_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/BFb0053381","volume-title":"ECOOP\u201997 \u2014 Object-Oriented Programming","author":"G Kiczales","year":"1997","unstructured":"Kiczales, G., et al.: Aspect-oriented programming. In: Ak\u015fit, M., Matsuoka, S. (eds.) ECOOP 1997. LNCS, vol. 1241, pp. 220\u2013242. Springer, Heidelberg (1997). \nhttps:\/\/doi.org\/10.1007\/BFb0053381"},{"doi-asserted-by":"crossref","unstructured":"Lange, J., Ng, N., Toninho, B., Yoshida, N.: Fencing off go: liveness and safety for channel-based programming. In: POPL, pp. 748\u2013761. ACM (2017)","key":"28_CR30","DOI":"10.1145\/3093333.3009847"},{"doi-asserted-by":"crossref","unstructured":"Lange, J., Ng, N., Toninho, B., Yoshida, N.: A static verification framework for message passing in go using behavioural types. In: ICSE, pp. 1137\u20131148. ACM (2018)","key":"28_CR31","DOI":"10.1145\/3180155.3180157"},{"doi-asserted-by":"crossref","unstructured":"L\u00f3pez, H.A., et al.: Protocol-based verification of message-passing parallel programs. In: OOPSLA, pp. 280\u2013298. ACM (2015)","key":"28_CR32","DOI":"10.1145\/2858965.2814302"},{"issue":"5","key":"28_CR33","doi-asserted-by":"publisher","first-page":"877","DOI":"10.1007\/s00165-017-0420-8","volume":"29","author":"R Neykova","year":"2017","unstructured":"Neykova, R., Bocchi, L., Yoshida, N.: Timed runtime monitoring for multiparty conversations. Formal Aspects Comput. 29(5), 877\u2013910 (2017). \nhttps:\/\/doi.org\/10.1007\/s00165-017-0420-8","journal-title":"Formal Aspects Comput."},{"doi-asserted-by":"crossref","unstructured":"Neykova, R., Hu, R., Yoshida, N., Abdeljallal, F.: A session type provider: compile-time API generation of distributed protocols with refinements in f#. In: CC, pp. 128\u2013138. ACM (2018)","key":"28_CR34","DOI":"10.1145\/3178372.3179495"},{"doi-asserted-by":"crossref","unstructured":"Neykova, R., Yoshida, N.: Let it recover: multiparty protocol-induced recovery. In: CC, pp. 98\u2013108. ACM (2017)","key":"28_CR35","DOI":"10.1145\/3033019.3033031"},{"doi-asserted-by":"crossref","unstructured":"Ng, N., Yoshida, N.: Static deadlock detection for concurrent go by global session graph synthesis. In: CC, pp. 174\u2013184. ACM (2016)","key":"28_CR36","DOI":"10.1145\/2892208.2892232"},{"key":"28_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-642-30561-0_15","volume-title":"Objects, Models, Components, Patterns","author":"N Ng","year":"2012","unstructured":"Ng, N., Yoshida, N., Honda, K.: Multiparty session C: safe parallel programming with message optimisation. In: Furia, C.A., Nanz, S. (eds.) TOOLS 2012. LNCS, vol. 7304, pp. 202\u2013218. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-30561-0_15"},{"unstructured":"Parlett, D.: The Penguin Book of Card Games. Penguin (2008)","key":"28_CR38"},{"key":"28_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-030-29852-4_5","volume-title":"Software Technology: Methods and Tools","author":"G Pinzaru","year":"2019","unstructured":"Pinzaru, G., Rivera, V.: Towards static verification of Clojure contract-based programs. In: Mazzara, M., Bruel, J.-M., Meyer, B., Petrenko, A. (eds.) TOOLS 2019. LNCS, vol. 11771, pp. 73\u201380. Springer, Cham (2019). \nhttps:\/\/doi.org\/10.1007\/978-3-030-29852-4_5"},{"unstructured":"Rust Team: Rust Programming Language (nd). \nhttps:\/\/rust-lang.org\n\n. Accessed 1 Sept 2019","key":"28_CR40"},{"doi-asserted-by":"crossref","unstructured":"Santos, C., Martins, F., Vasconcelos, V.T.: Deductive verification of parallel programs using why3. In: ICE. EPTCS, vol. 189, pp. 128\u2013142 (2015)","key":"28_CR41","DOI":"10.4204\/EPTCS.189.11"},{"unstructured":"Scalas, A., Dardha, O., Hu, R., Yoshida, N.: A linear decomposition of multiparty sessions for safe distributed programming. In: ECOOP. LIPIcs, vol. 74, pp. 24:1\u201324:31. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017)","key":"28_CR42"},{"key":"28_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-319-47958-3_7","volume-title":"Programming Languages and Systems","author":"K Stadtm\u00fcller","year":"2016","unstructured":"Stadtm\u00fcller, K., Sulzmann, M., Thiemann, P.: Static trace-based deadlock analysis for synchronous mini-go. In: Igarashi, A. (ed.) APLAS 2016. LNCS, vol. 10017, pp. 116\u2013136. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-47958-3_7"},{"key":"28_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/978-3-642-39038-8_13","volume-title":"ECOOP 2013 \u2013 Object-Oriented Programming","author":"S Tasharofi","year":"2013","unstructured":"Tasharofi, S., Dinges, P., Johnson, R.E.: Why do Scala developers mix the actor model with other concurrency models? In: Castagna, G. (ed.) ECOOP 2013. LNCS, vol. 7920, pp. 302\u2013326. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-39038-8_13"},{"doi-asserted-by":"crossref","unstructured":"Tu, T., Liu, X., Song, L., Zhang, Y.: Understanding real-world concurrency bugs in go. In: ASPLOS, pp. 865\u2013878. ACM (2019)","key":"28_CR45","DOI":"10.1145\/3297858.3304069"},{"key":"28_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-030-36987-3_5","volume-title":"Distributed Computing and Internet Technology","author":"N Yoshida","year":"2020","unstructured":"Yoshida, N., Gheri, L.: A very gentle introduction to multiparty session types. In: Hung, D.V., D\u2019Souza, M. (eds.) ICDCIT 2020. LNCS, vol. 11969, pp. 73\u201393. Springer, Cham (2020). \nhttps:\/\/doi.org\/10.1007\/978-3-030-36987-3_5"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-61362-4_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,28]],"date-time":"2020-10-28T13:13:36Z","timestamp":1603890816000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-61362-4_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030613617","9783030613624"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-61362-4_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"29 October 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rhodes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 October 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 October 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/isola-conference.org\/isola2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}