{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,17]],"date-time":"2025-10-17T19:50:37Z","timestamp":1760730637299},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662442012"},{"type":"electronic","value":"9783662442029"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-662-44202-9_14","type":"book-chapter","created":{"date-parts":[[2014,7,17]],"date-time":"2014-07-17T02:01:13Z","timestamp":1405562473000},"page":"334-359","source":"Crossref","is-referenced-by-count":5,"title":["Rely-Guarantee Protocols"],"prefix":"10.1007","author":[{"given":"Filipe","family":"Milit\u00e3o","sequence":"first","affiliation":[]},{"given":"Jonathan","family":"Aldrich","sequence":"additional","affiliation":[]},{"given":"Lu\u00eds","family":"Caires","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","unstructured":"Ahmed, A., Fluet, M., Morrisett, G.: L3: A linear language with locations. Fundam. Inf. (2007)"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Beckman, N.E., Bierhoff, K., Aldrich, J.: Verifying correct usage of atomic blocks and typestate. In: OOPSLA (2008)","DOI":"10.21236\/ADA487668"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-22655-7_2","volume-title":"ECOOP 2011 \u2013 Object-Oriented Programming","author":"N.E. Beckman","year":"2011","unstructured":"Beckman, N.E., Kim, D., Aldrich, J.: An empirical study of object protocols in the wild. In: Mezini, M. (ed.) ECOOP 2011. LNCS, vol.\u00a06813, pp. 2\u201326. Springer, Heidelberg (2011)"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Bierhoff, K., Aldrich, J.: Modular typestate checking of aliased objects. In: OOPSLA (2007)","DOI":"10.21236\/ADA465507"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"Caires, L., Seco, J.A.C.: The type discipline of behavioral separation. In: POPL (2013)","DOI":"10.1145\/2429069.2429103"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Calcagno, C., O\u2019Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: Proc. Logic in Computer Science (2007)","DOI":"10.1109\/LICS.2007.30"},{"key":"14_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/978-3-540-24851-4_21","volume-title":"ECOOP 2004 \u2013 Object-Oriented Programming","author":"R. DeLine","year":"2004","unstructured":"DeLine, R., F\u00e4hndrich, M.: Typestates for objects. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol.\u00a03086, pp. 465\u2013490. Springer, Heidelberg (2004)"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M., Yang, H.: Views: compositional reasoning for concurrent programs. In: POPL (2013)","DOI":"10.1145\/2429069.2429104"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-642-14107-2_24","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"T. Dinsdale-Young","year":"2010","unstructured":"Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M.J., Vafeiadis, V.: Concurrent abstract predicates. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol.\u00a06183, pp. 504\u2013528. Springer, Heidelberg (2010)"},{"key":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/978-3-642-00590-9_26","volume-title":"Programming Languages and Systems","author":"M. Dodds","year":"2009","unstructured":"Dodds, M., Feng, X., Parkinson, M., Vafeiadis, V.: Deny-guarantee reasoning. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol.\u00a05502, pp. 363\u2013377. Springer, Heidelberg (2009)"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"F\u00e4hndrich, M., DeLine, R.: Adoption and focus: practical linear types for imperative programming. In: PLDI (2002)","DOI":"10.1145\/512530.512532"},{"key":"14_CR12","unstructured":"F\u00e4hndrich, M., Leino, K.R.M.: Heap monotonic typestate. In: IWACO (2003)"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"Gay, S.J., Vasconcelos, V.T., Ravara, A., Gesbert, N., Caldeira, A.Z.: Modular session types for distributed object-oriented programming. In: POPL (2010)","DOI":"10.1145\/1706299.1706335"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Girard, J.-Y.: Linear logic. Theor. Comput. Sci. (1987)","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Gordon, C.S., Ernst, M.D., Grossman, D.: Rely-guarantee references for refinement types over aliased mutable data. In: PLDI (2013)","DOI":"10.1145\/2491956.2462160"},{"key":"14_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/978-3-642-28869-2_19","volume-title":"Programming Languages and Systems","author":"J.B. Jensen","year":"2012","unstructured":"Jensen, J.B., Birkedal, L.: Fictional separation logic. In: Seidl, H. (ed.) Programming Languages and Systems. LNCS, vol.\u00a07211, pp. 377\u2013396. Springer, Heidelberg (2012)"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. (1983)","DOI":"10.1145\/69575.69577"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Krishnaswami, N.R., Turon, A., Dreyer, D., Garg, D.: Superficially substructural types. In: ICFP (2012)","DOI":"10.1145\/2364527.2364536"},{"key":"14_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-642-00590-9_27","volume-title":"Programming Languages and Systems","author":"K.R.M. Leino","year":"2009","unstructured":"Leino, K.R.M., M\u00fcller, P.: A basis for verifying multi-threaded programs. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol.\u00a05502, pp. 378\u2013393. Springer, Heidelberg (2009)"},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"Mandelbaum, Y., Walker, D., Harper, R.: An effective theory of type refinements. In: ICFP (2003)","DOI":"10.1145\/944705.944725"},{"key":"14_CR21","doi-asserted-by":"crossref","unstructured":"Milit\u00e3o, F., Aldrich, J., Caires, L.: Rely-guarantee protocols (technical report). CMU-CS-14-107 (2014)","DOI":"10.21236\/ADA605817"},{"key":"14_CR22","doi-asserted-by":"crossref","unstructured":"Milit\u00e3o, F., Aldrich, J., Caires, L.: Substructural typestates. In: PLPV (2014)","DOI":"10.1145\/2541568.2541574"},{"key":"14_CR23","doi-asserted-by":"crossref","unstructured":"Parkinson, M., Bierman, G.: Separation logic and abstraction. In: POPL (2005)","DOI":"10.1145\/1040305.1040326"},{"key":"14_CR24","doi-asserted-by":"crossref","unstructured":"Pilkiewicz, A., Pottier, F.: The essence of monotonic state. In: TLDI (2011)","DOI":"10.1145\/1929553.1929565"},{"key":"14_CR25","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proc. Logic in Computer Science (2002)"},{"key":"14_CR26","doi-asserted-by":"crossref","unstructured":"Sabry, A., Felleisen, M.: Reasoning about programs in continuation-passing style. In: Proc. LISP and Functional Programming (1992)","DOI":"10.1145\/141471.141563"},{"key":"14_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/3-540-46425-5_24","volume-title":"Programming Languages and Systems","author":"F. Smith","year":"2000","unstructured":"Smith, F., Walker, D.W., Morrisett, G.: Alias types. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol.\u00a01782, pp. 366\u2013381. Springer, Heidelberg (2000)"},{"key":"14_CR28","doi-asserted-by":"crossref","unstructured":"Strom, R.E.: Mechanisms for compile-time enforcement of security. In: POPL (1983)","DOI":"10.1145\/567067.567093"},{"key":"14_CR29","doi-asserted-by":"crossref","unstructured":"Strom, R.E., Yemini, S.: Typestate: A programming language concept for enhancing software reliability. IEEE Trans. Software Eng. (1986)","DOI":"10.1109\/TSE.1986.6312929"},{"key":"14_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-642-37036-6_11","volume-title":"Programming Languages and Systems","author":"K. Svendsen","year":"2013","unstructured":"Svendsen, K., Birkedal, L., Parkinson, M.: Modular reasoning about separation of concurrent data structures. In: Felleisen, M., Gardner, P. (eds.) Programming Languages and Systems. LNCS, vol.\u00a07792, pp. 169\u2013188. Springer, Heidelberg (2013)"},{"key":"14_CR31","doi-asserted-by":"crossref","unstructured":"Tov, J.A., Pucella, R.: Practical affine types. In: POPL (2011)","DOI":"10.1145\/1926385.1926436"},{"key":"14_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-540-74407-8_18","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"V. Vafeiadis","year":"2007","unstructured":"Vafeiadis, V., Parkinson, M.: A marriage of rely\/Guarantee and separation logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol.\u00a04703, pp. 256\u2013271. Springer, Heidelberg (2007)"},{"key":"14_CR33","doi-asserted-by":"crossref","unstructured":"Yorsh, G., Skidanov, A., Reps, T., Sagiv, M.: Automatic assume\/guarantee reasoning for heap-manipulating programs. Electron. Notes Theor. Comput. Sci. (2005)","DOI":"10.1016\/j.entcs.2005.01.028"}],"container-title":["Lecture Notes in Computer Science","ECOOP 2014 \u2013 Object-Oriented Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-44202-9_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,12]],"date-time":"2019-08-12T22:30:01Z","timestamp":1565649001000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-44202-9_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783662442012","9783662442029"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-44202-9_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}