{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:13:49Z","timestamp":1775873629995,"version":"3.50.1"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319898834","type":"print"},{"value":"9783319898841","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-89884-1_28","type":"book-chapter","created":{"date-parts":[[2018,4,13]],"date-time":"2018-04-13T21:02:32Z","timestamp":1523653352000},"page":"799-826","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["A Typing Discipline for Statically Verified Crash Failure Handling in Distributed Systems"],"prefix":"10.1007","author":[{"given":"Malte","family":"Viering","sequence":"first","affiliation":[]},{"given":"Tzu-Chun","family":"Chen","sequence":"additional","affiliation":[]},{"given":"Patrick","family":"Eugster","sequence":"additional","affiliation":[]},{"given":"Raymond","family":"Hu","sequence":"additional","affiliation":[]},{"given":"Lukasz","family":"Ziarek","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,4,14]]},"reference":[{"key":"28_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-60225-7_1","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"M Adameit","year":"2017","unstructured":"Adameit, M., Peters, K., Nestmann, U.: Session types for link failures. In: Bouajjani, A., Silva, A. (eds.) FORTE 2017. LNCS, vol. 10321, pp. 1\u201316. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-60225-7_1"},{"key":"28_CR2","unstructured":"Armstrong, J.: Making reliable distributed systems in the presence of software errors. Ph.D. thesis, Royal Institute of Technology, Stockholm, Sweden (2003)"},{"key":"28_CR3","unstructured":"Birman, K.P.: Byzantine Clients (2017). https:\/\/goo.gl\/1Qbc4r"},{"key":"28_CR4","unstructured":"Burrows, M.: The Chubby lock service for loosely-coupled distributed systems. In: OSDI 2006, pp. 335\u2013350. USENIX Association (2006)"},{"key":"28_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/978-3-319-39570-8_6","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"L Caires","year":"2016","unstructured":"Caires, L., P\u00e9rez, J.A.: Multiparty session types within a canonical binary theory, and beyond. In: Albert, E., Lanese, I. (eds.) FORTE 2016. LNCS, vol. 9688, pp. 74\u201395. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-39570-8_6"},{"issue":"2","key":"28_CR6","first-page":"156","volume":"26","author":"S Capecchi","year":"2016","unstructured":"Capecchi, S., Giachino, E., Yoshida, N.: Global escape in multiparty sessions. MSCS 26(2), 156\u2013205 (2016)","journal-title":"MSCS"},{"key":"28_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1007\/978-3-540-85361-9_32","volume-title":"CONCUR 2008 - Concurrency Theory","author":"M Carbone","year":"2008","unstructured":"Carbone, M., Honda, K., Yoshida, N.: Structured interactional exceptions in session types. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 402\u2013417. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-85361-9_32"},{"key":"28_CR8","unstructured":"Carbone, M., Lindley, S., Montesi, F., Sch\u00fcrmann, C., Wadler, P.: Coherence generalises duality: a logical explanation of multiparty session types. In: CONCUR 2016. LIPIcs, vol. 59, pp. 33:1\u201333:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016)"},{"key":"28_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-642-01918-0_5","volume-title":"Formal Methods for Web Services","author":"M Carbone","year":"2009","unstructured":"Carbone, M., Yoshida, N., Honda, K.: Asynchronous session types: exceptions and multiparty interactions. In: Bernardo, M., Padovani, L., Zavattaro, G. (eds.) SFM 2009. LNCS, vol. 5569, pp. 187\u2013212. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-01918-0_5"},{"key":"28_CR10","doi-asserted-by":"crossref","unstructured":"Chandra, T.D., Hadzilacos, V., Toueg, S., Charron-Bost, B.: On the impossibility of group membership. In: PODC 1996, pp. 322\u2013330. ACM (1996)","DOI":"10.1145\/248052.248120"},{"key":"28_CR11","unstructured":"Chang, F., Dean, J., Ghemawat, S., Hsieh, W.C., Wallach, D.A., Burrows, M., Chandra, T., Fikes, A., Gruber, R.: Bigtable: a distributed storage system for structured data. In: OSDI 2006, pp. 205\u2013218. USENIX Association (2006)"},{"issue":"1","key":"28_CR12","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/s00446-009-0084-6","volume":"22","author":"B Charron-Bost","year":"2009","unstructured":"Charron-Bost, B., Schiper, A.: The Heard-Of model: computing in distributed systems with benign faults. Distrib. Comput. 22(1), 49\u201371 (2009)","journal-title":"Distrib. Comput."},{"key":"28_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-319-39570-8_7","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"T-C Chen","year":"2016","unstructured":"Chen, T.-C., Viering, M., Bejleri, A., Ziarek, L., Eugster, P.: A type theory for robust failure handling in distributed systems. In: Albert, E., Lanese, I. (eds.) FORTE 2016. LNCS, vol. 9688, pp. 96\u2013113. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-39570-8_7"},{"key":"28_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-319-18941-3_4","volume-title":"Formal Methods for Multicore Programming","author":"M Coppo","year":"2015","unstructured":"Coppo, M., Dezani-Ciancaglini, M., Padovani, L., Yoshida, N.: A gentle introduction to multiparty asynchronous session types. In: Bernardo, M., Johnsen, E.B. (eds.) SFM 2015. LNCS, vol. 9104, pp. 146\u2013178. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-18941-3_4"},{"issue":"2","key":"28_CR15","first-page":"238","volume":"26","author":"M Coppo","year":"2016","unstructured":"Coppo, M., Dezani-Ciancaglini, M., Yoshida, N., Padovani, L.: Global progress for dynamically interleaved multiparty sessions. MSCS 26(2), 238\u2013302 (2016)","journal-title":"MSCS"},{"issue":"3","key":"28_CR16","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. Formal Methods Syst. Des. 46(3), 197\u2013225 (2015)","journal-title":"Formal Methods Syst. Des."},{"key":"28_CR17","doi-asserted-by":"crossref","unstructured":"Deni\u00e9lou, P.M., Yoshida, N.: Dynamic multirole session types. In: POPL 2011, pp. 435\u2013446. ACM (2011)","DOI":"10.1145\/1925844.1926435"},{"issue":"1","key":"28_CR18","doi-asserted-by":"publisher","first-page":"400","DOI":"10.1145\/2914770.2837650","volume":"51","author":"Cezara Dr\u0103goi","year":"2016","unstructured":"Dragoi, C., Henzinger, T., Zufferey, D.: PSync: a partially synchronous language for fault-tolerant distributed algorithms. In: POPL 2016, pp. 400\u2013415. ACM (2016)","journal-title":"ACM SIGPLAN Notices"},{"issue":"2","key":"28_CR19","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1145\/3149.214121","volume":"32","author":"MJ Fischer","year":"1985","unstructured":"Fischer, M.J., Lynch, N.A., Paterson, M.S.: Impossibility of distributed consensus with one faulty process. J. ACM 32(2), 374\u2013382 (1985)","journal-title":"J. ACM"},{"key":"28_CR20","doi-asserted-by":"crossref","unstructured":"Ghemawat, S., Gobioff, H., Leung, S.T.: The Google file system. In: SOSP 2003, pp. 29\u201343. ACM (2003)","DOI":"10.1145\/945445.945450"},{"issue":"2","key":"28_CR21","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1145\/564585.564601","volume":"33","author":"S Gilbert","year":"2002","unstructured":"Gilbert, S., Lynch, N.: Brewer\u2019s conjecture and the feasibility of consistent, available, partition-tolerant web services. SIGACT News 33(2), 51\u201359 (2002)","journal-title":"SIGACT News"},{"issue":"1","key":"28_CR22","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1109\/32.895986","volume":"27","author":"R Guerraoui","year":"2001","unstructured":"Guerraoui, R., Schiper, A.: The generic consensus service. IEEE Trans. Softw. Eng. 27(1), 29\u201341 (2001)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"28_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/BFb0053567","volume-title":"Programming Languages and Systems","author":"K Honda","year":"1998","unstructured":"Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 122\u2013138. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0053567"},{"issue":"1","key":"28_CR24","doi-asserted-by":"publisher","first-page":"9:1","DOI":"10.1145\/2827695","volume":"63","author":"K Honda","year":"2016","unstructured":"Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. J. ACM 63(1), 9:1\u20139:67 (2016)","journal-title":"J. ACM"},{"key":"28_CR25","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). https:\/\/doi.org\/10.1007\/978-3-662-49665-7_24"},{"key":"28_CR26","unstructured":"Hunt, P.: ZooKeeper: wait-free coordination for internet-scale systems. In: USENIX 2010. USENIX Association (2010)"},{"issue":"1","key":"28_CR27","doi-asserted-by":"publisher","first-page":"3:1","DOI":"10.1145\/2873052","volume":"49","author":"H H\u00fcttel","year":"2016","unstructured":"H\u00fcttel, H., et al.: Foundations of session types and behavioural contracts. ACM Comput. Surv. 49(1), 3:1\u20133:36 (2016)","journal-title":"ACM Comput. Surv."},{"key":"28_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-319-59746-1_6","volume-title":"Coordination Models and Languages","author":"K Imai","year":"2017","unstructured":"Imai, K., Yoshida, N., Yuen, S.: Session-ocaml: a session-based library with polarities and lenses. In: Jacquet, J.-M., Massink, M. (eds.) COORDINATION 2017. LNCS, vol. 10319, pp. 99\u2013118. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-59746-1_6"},{"key":"28_CR29","doi-asserted-by":"crossref","unstructured":"Killian, C.E., Anderson, J.W., Braud, R., Jhala, R., Vahdat, A.M.: Mace: language support for building distributed systems. In: PLDI 2007, vol. 42, pp. 179\u2013188. ACM (2007)","DOI":"10.1145\/1250734.1250755"},{"issue":"4","key":"28_CR30","first-page":"1","volume":"10","author":"D Kouzapas","year":"2014","unstructured":"Kouzapas, D., Yoshida, N.: Globally governed session semantics. LMCS 10(4), 1\u201345 (2014)","journal-title":"LMCS"},{"key":"28_CR31","unstructured":"Kreps, J., Narkhede, N., Rao, J.: Kafka: a distributed messaging system for log processing. In: NetDB 2011 (2011)"},{"issue":"3","key":"28_CR32","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1145\/357172.357176","volume":"4","author":"L Lamport","year":"1982","unstructured":"Lamport, L., Shostak, R., Pease, M.: The Byzantine generals problem. ACM Trans. Program. Lang. Syst. 4(3), 382\u2013401 (1982)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"28_CR33","doi-asserted-by":"crossref","unstructured":"Leners, J.B., Wu, H., Hung, W.L., Aguilera, M.K., Walfish, M.: Detecting failures in distributed systems with the FALCON spy network. In: SOSP 2011, pp. 279\u2013294. ACM (2011)","DOI":"10.1145\/2043556.2043583"},{"key":"28_CR34","doi-asserted-by":"crossref","unstructured":"Lindley, S., Morris, J.G.: embedding session types in haskell. In: Haskell 2016, pp. 133\u2013145. ACM (2016)","DOI":"10.1145\/3241625.2976018"},{"key":"28_CR35","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/j.ic.2015.02.002","volume":"241","author":"D Mostrous","year":"2015","unstructured":"Mostrous, D., Yoshida, N.: Session typing and asynchronous subtyping for the higher-order $$\\pi $$\u03c0-calculus. Inf. Comput. 241, 227\u2013263 (2015)","journal-title":"Inf. Comput."},{"key":"28_CR36","doi-asserted-by":"crossref","unstructured":"Neykova, R., Yoshida, N.: Let it recover: multiparty protocol-induced recovery. In: CC 2017, pp. 98\u2013108. ACM (2017)","DOI":"10.1145\/3033019.3033031"},{"key":"28_CR37","doi-asserted-by":"publisher","first-page":"e4","DOI":"10.1017\/S0956796816000289","volume":"27","author":"L Padovani","year":"2017","unstructured":"Padovani, L.: A simple library implementation of binary sessions. J. Funct. Program. 27, e4 (2017)","journal-title":"J. Funct. Program."},{"key":"28_CR38","doi-asserted-by":"crossref","unstructured":"Pucella, R., Tov, J.A.: Haskell session types with (almost) no class. In: Haskell 2008, pp. 25\u201336. ACM (2008)","DOI":"10.1145\/1411286.1411290"},{"key":"28_CR39","unstructured":"Scalas, A., Dardha, O., Hu, R., Yoshida, N.: A linear decomposition of multiparty sessions for safe distributed programming. In: ECOOP 2017. LIPIcs, vol. 74, pp. 24:1\u201324:31. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017)"},{"key":"28_CR40","doi-asserted-by":"crossref","unstructured":"Shvachko, K., Kuang, H., Radia, S., Chansler, R.: The Hadoop distributed file system. In: MSST 2010, pp. 1\u201310. IEEE Computer Society (2010)","DOI":"10.1109\/MSST.2010.5496972"},{"issue":"2","key":"28_CR41","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/j.scico.2012.03.004","volume":"78","author":"KC Sivaramakrishnan","year":"2013","unstructured":"Sivaramakrishnan, K.C., Qudeisat, M., Ziarek, L., Nagaraj, K., Eugster, P.: Efficient sessions. Sci. Comput. Program. 78(2), 147\u2013167 (2013)","journal-title":"Sci. Comput. Program."},{"key":"28_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-540-78739-6_21","volume-title":"Programming Languages and Systems","author":"HT Vieira","year":"2008","unstructured":"Vieira, H.T., Caires, L., Seco, J.C.: The conversation calculus: a model of service-oriented computation. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 269\u2013283. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78739-6_21"},{"key":"28_CR43","doi-asserted-by":"crossref","unstructured":"Viering, M., Chen, T.C., Eugster, P., Hu, R., Ziarek, L.: Technical appendix: a typing discipline for statically verified crash failure handling in distributed systems. http:\/\/distributed-systems-programming-group.github.io\/paper\/2018\/esop_long.pdf","DOI":"10.1007\/978-3-319-89884-1_28"},{"issue":"6","key":"28_CR44","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1145\/2813885.2737958","volume":"50","author":"James R. Wilcox","year":"2015","unstructured":"Wilcox, J.R., Woos, D., Panchekha, P., Tatlock, Z., Wang, X., Ernst, M.D., Anderson, T.E.: Verdi: a framework for implementing and formally verifying distributed systems. In: PLDI 2015, pp. 357\u2013368. ACM (2015)","journal-title":"ACM SIGPLAN Notices"},{"key":"28_CR45","unstructured":"Xu, J., Randell, B., Romanovsky, A.B., Rubira, C.M.F., Stroud, R.J., Wu, Z.: Fault tolerance in concurrent object-oriented software through coordinated error recovery. In: FTCS 1995, pp. 499\u2013508. IEEE Computer Society (1995)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-89884-1_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,15]],"date-time":"2019-10-15T16:33:23Z","timestamp":1571157203000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89884-1_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319898834","9783319898841"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89884-1_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}