{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,7]],"date-time":"2026-07-07T03:00:47Z","timestamp":1783393247780,"version":"3.54.6"},"publisher-location":"Berlin, Heidelberg","reference-count":41,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662544334","type":"print"},{"value":"9783662544341","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-662-54434-1_34","type":"book-chapter","created":{"date-parts":[[2017,3,18]],"date-time":"2017-03-18T04:20:06Z","timestamp":1489810806000},"page":"909-936","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":39,"title":["A Higher-Order Logic for Concurrent Termination-Preserving Refinement"],"prefix":"10.1007","author":[{"given":"Joseph","family":"Tassarotti","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ralf","family":"Jung","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Robert","family":"Harper","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,3,19]]},"reference":[{"key":"34_CR1","unstructured":"Website with Coq development (2016). http:\/\/www.cs.cmu.edu\/~jtassaro\/papers\/iris-refinement"},{"issue":"5","key":"34_CR2","doi-asserted-by":"publisher","first-page":"657","DOI":"10.1145\/504709.504712","volume":"23","author":"A Appel","year":"2001","unstructured":"Appel, A., McAllester, D.: An indexed model of recursive types for foundational proof-carrying code. TOPLAS 23(5), 657\u2013683 (2001)","journal-title":"TOPLAS"},{"key":"34_CR3","doi-asserted-by":"crossref","unstructured":"Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: POPL (2004)","DOI":"10.1145\/964001.964003"},{"issue":"4","key":"34_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-9(4:4)2013","volume":"9","author":"L Birkedal","year":"2013","unstructured":"Birkedal, L., Bizjak, A., Schwinghammer, J.: Step-indexed relational reasoning for countable nondeterminism. Logical Methods Comput. Sci. 9(4), 1\u201322 (2013)","journal-title":"Logical Methods Comput. Sci."},{"issue":"47","key":"34_CR5","doi-asserted-by":"publisher","first-page":"4102","DOI":"10.1016\/j.tcs.2010.07.010","volume":"411","author":"L Birkedal","year":"2010","unstructured":"Birkedal, L., St\u00f8vring, K., Thamsborg, J.: The category-theoretic solution of recursive metric-space equations. Theor. Comput. Sci. 411(47), 4102\u20134122 (2010)","journal-title":"Theor. Comput. Sci."},{"key":"34_CR6","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1016\/j.entcs.2006.04.008","volume":"158","author":"SD Brookes","year":"2006","unstructured":"Brookes, S.D.: Variables as resource for shared-memory programs: semantics and soundness. Electr. Notes Theor. Comput. Sci. 158, 123\u2013150 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"34_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1007\/978-3-642-37036-6_19","volume-title":"Programming Languages and Systems","author":"L Caires","year":"2013","unstructured":"Caires, L., P\u00e9rez, J.A., Pfenning, F., Toninho, B.: Behavioral polymorphism and parametricity in session-based communication. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 330\u2013349. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-37036-6_19"},{"key":"34_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/978-3-642-15375-4_16","volume-title":"CONCUR 2010 - Concurrency Theory","author":"L Caires","year":"2010","unstructured":"Caires, L., Pfenning, F.: Session types as intuitionistic linear propositions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 222\u2013236. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-15375-4_16"},{"key":"34_CR9","unstructured":"Craig, T.S.: Building fifo and priority-queueing spin locks from atomic swap. Technical report 93-02-02, Computer Science Department, University of Washington (1993)"},{"key":"34_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-662-44202-9_9","volume-title":"ECOOP 2014 \u2013 Object-Oriented Programming","author":"P da Rocha Pinto","year":"2014","unstructured":"da Rocha Pinto, P., Dinsdale-Young, T., Gardner, P.: TaDA: a logic for time and data abstraction. In: Jones, R. (ed.) ECOOP 2014. LNCS, vol. 8586, pp. 207\u2013231. Springer, Heidelberg (2014). doi:10.1007\/978-3-662-44202-9_9"},{"key":"34_CR11","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. 6183, pp. 504\u2013528. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-14107-2_24"},{"key":"34_CR12","doi-asserted-by":"crossref","unstructured":"Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M.J., Yang, H.: Views: compositional reasoning for concurrent programs. In: POPL (2013)","DOI":"10.1145\/2429069.2429104"},{"key":"34_CR13","doi-asserted-by":"crossref","unstructured":"Feng, X.: Local rely-guarantee reasoning. In: POPL, pp. 315\u2013327 (2009)","DOI":"10.1145\/1594834.1480922"},{"issue":"1","key":"34_CR14","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1017\/S0956796809990268","volume":"20","author":"SJ Gay","year":"2010","unstructured":"Gay, S.J., Vasconcelos, V.T.: Linear type theory for asynchronous session types. J. Funct. Program. 20(1), 19\u201350 (2010)","journal-title":"J. Funct. Program."},{"key":"34_CR15","doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Marmar, M., Shao, Z.: Quantitative reasoning for proving lock-freedom. In: LICS, pp. 124\u2013133 (2013)","DOI":"10.1109\/LICS.2013.18"},{"key":"34_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1007\/3-540-57208-2_35","volume-title":"CONCUR\u201993","author":"K Honda","year":"1993","unstructured":"Honda, K.: Types for dyadic interaction. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 509\u2013523. Springer, Heidelberg (1993). doi:10.1007\/3-540-57208-2_35"},{"key":"34_CR17","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S.S., O\u2019Hearn, P.W.: BI as an assertion language for mutable data structures. In: POPL, pp. 14\u201326 (2001)","DOI":"10.1145\/373243.375719"},{"issue":"4","key":"34_CR18","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"CB Jones","year":"1983","unstructured":"Jones, C.B.: Tentative steps toward a development method for interfering programs. TOPLAS 5(4), 596\u2013619 (1983)","journal-title":"TOPLAS"},{"key":"34_CR19","doi-asserted-by":"crossref","unstructured":"Jung, R., Krebbers, R., Birkedal, L., Dreyer, D.: Higher-order ghost state. In: ICFP, pp. 256\u2013269 (2016, to appear)","DOI":"10.1145\/3022670.2951943"},{"key":"34_CR20","doi-asserted-by":"crossref","unstructured":"Jung, R., Swasey, D., Sieczkowski, F., Svendsen, K., Turon, A., Birkedal, L., Dreyer, D.: Iris: monoids and invariants as an orthogonal basis for concurrent reasoning. In: POPL, pp. 637\u2013650 (2015)","DOI":"10.1145\/2775051.2676980"},{"key":"34_CR21","doi-asserted-by":"crossref","unstructured":"Krebbers, R., Timany, A., Birkedal, L.: Interactive proofs in higher-order concurrent separation logic. In: POPL, pp. 205\u2013217 (2017, to appear)","DOI":"10.1145\/3093333.3009855"},{"key":"34_CR22","doi-asserted-by":"crossref","unstructured":"Krogh-Jespersen, M., Svendsen, K., Birkedal, L.: A relational model of types-and-effects in higher-order concurrent separation logic. In: POPL, pp. 218\u2013231 (2017, to appear)","DOI":"10.1145\/3093333.3009877"},{"key":"34_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1007\/3-540-10843-2_22","volume-title":"Automata, Languages and Programming","author":"D Lehmann","year":"1981","unstructured":"Lehmann, D., Pnueli, A., Stavi, J.: Impartiality, justice and fairness: the ethics of concurrent termination. In: Even, S., Kariv, O. (eds.) ICALP 1981. LNCS, vol. 115, pp. 264\u2013277. Springer, Heidelberg (1981). doi:10.1007\/3-540-10843-2_22"},{"key":"34_CR24","doi-asserted-by":"crossref","unstructured":"Liang, H., Feng, X.: A program logic for concurrent objects under fair scheduling. In: POPL, pp. 385\u2013399 (2016)","DOI":"10.1145\/2914770.2837635"},{"issue":"1","key":"34_CR25","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1145\/2576235","volume":"36","author":"H Liang","year":"2014","unstructured":"Liang, H., Feng, X., Fu, M.: Rely-guarantee-based simulation for compositional verification of concurrent program transformations. ACM Trans. Program. Lang. Syst. 36(1), 3 (2014)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"34_CR26","doi-asserted-by":"crossref","unstructured":"Liang, H., Feng, X., Shao, Z.: Compositional verification of termination-preserving refinement of concurrent programs. In: CSL-LICS, pp. 65:1\u201365:10 (2014)","DOI":"10.1145\/2603088.2603123"},{"key":"34_CR27","doi-asserted-by":"crossref","unstructured":"Magnusson, P.S., Landin, A., Hagersten, E.: Queue locks on cache coherent multiprocessors. In: International Symposium on Parallel Processing, pp. 165\u2013171 (1994)","DOI":"10.1109\/IPPS.1994.288305"},{"key":"34_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-642-54833-8_16","volume-title":"Programming Languages and Systems","author":"A Nanevski","year":"2014","unstructured":"Nanevski, A., Ley-Wild, R., Sergey, I., Delbianco, G.A.: Communicating state transition systems for fine-grained concurrent resources. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 290\u2013310. Springer, Heidelberg (2014). doi:10.1007\/978-3-642-54833-8_16"},{"issue":"1","key":"34_CR29","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"P O\u2019Hearn","year":"2007","unstructured":"O\u2019Hearn, P.: Resources, concurrency, and local reasoning. TCS 375(1), 271\u2013307 (2007)","journal-title":"TCS"},{"key":"34_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"539","DOI":"10.1007\/978-3-642-28869-2_27","volume-title":"Programming Languages and Systems","author":"JA P\u00e9rez","year":"2012","unstructured":"P\u00e9rez, J.A., Caires, L., Pfenning, F., Toninho, B.: Linear logical relations for session-based concurrency. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 539\u2013558. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-28869-2_27"},{"key":"34_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/978-3-662-49498-1_8","volume-title":"Programming Languages and Systems","author":"P da Rocha Pinto","year":"2016","unstructured":"da Rocha Pinto, P., Dinsdale-Young, T., Gardner, P., Sutherland, J.: Modular termination verification for non-blocking concurrency. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 176\u2013201. Springer, Heidelberg (2016). doi:10.1007\/978-3-662-49498-1_8"},{"key":"34_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-642-54833-8_9","volume-title":"Programming Languages and Systems","author":"K Svendsen","year":"2014","unstructured":"Svendsen, K., Birkedal, L.: Impredicative concurrent abstract predicates. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 149\u2013168. Springer, Heidelberg (2014). doi:10.1007\/978-3-642-54833-8_9"},{"key":"34_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"727","DOI":"10.1007\/978-3-662-49498-1_28","volume-title":"Programming Languages and Systems","author":"K Svendsen","year":"2016","unstructured":"Svendsen, K., Sieczkowski, F., Birkedal, L.: Transfinite step-indexing: decoupling concrete and logical steps. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 727\u2013751. Springer, Heidelberg (2016). doi:10.1007\/978-3-662-49498-1_28"},{"key":"34_CR34","doi-asserted-by":"crossref","unstructured":"Tassarotti, J., Jung, R., Harper, R.: A higher-order logic for concurrent termination-preserving refinement. Available as arXiv:1701.05888 [cs.PL] (2017). http:\/\/iris-project.org\/pdfs\/2017-esop-refinement-final.pdf. Extended version with appendices","DOI":"10.1007\/978-3-662-54434-1_34"},{"key":"34_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/978-3-642-37036-6_20","volume-title":"Programming Languages and Systems","author":"B Toninho","year":"2013","unstructured":"Toninho, B., Caires, L., Pfenning, F.: Higher-order processes, functions, and sessions: a monadic integration. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 350\u2013369. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-37036-6_20"},{"key":"34_CR36","doi-asserted-by":"crossref","unstructured":"Turon, A., Dreyer, D., Birkedal, L.: Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency. In: ICFP, pp. 377\u2013390 (2013)","DOI":"10.1145\/2544174.2500600"},{"key":"34_CR37","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. 4703, pp. 256\u2013271. Springer, Heidelberg (2007). doi:10.1007\/978-3-540-74407-8_18"},{"issue":"2\u20133","key":"34_CR38","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1017\/S095679681400001X","volume":"24","author":"P Wadler","year":"2014","unstructured":"Wadler, P.: Propositions as sessions. J. Funct. Program. 24(2\u20133), 384\u2013418 (2014)","journal-title":"J. Funct. Program."},{"key":"34_CR39","doi-asserted-by":"crossref","unstructured":"Willsey, M., Prabhu, R., Pfenning, F.: Design and implementation of concurrent C0. In: Linearity (2016)","DOI":"10.4204\/EPTCS.238.8"},{"issue":"1\u20133","key":"34_CR40","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1016\/j.tcs.2006.12.036","volume":"375","author":"H Yang","year":"2007","unstructured":"Yang, H.: Relational separation logic. TCS 375(1\u20133), 308\u2013334 (2007)","journal-title":"TCS"},{"issue":"4","key":"34_CR41","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/j.entcs.2007.02.056","volume":"171","author":"N Yoshida","year":"2007","unstructured":"Yoshida, N., Vasconcelos, V.T.: Language primitives and type discipline for structured communication-based programming revisited: Two systems for higher-order session communication. Electr. Notes Theor. Comput. Sci. 171(4), 73\u201393 (2007)","journal-title":"Electr. Notes Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-54434-1_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T01:41:38Z","timestamp":1750124498000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-54434-1_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783662544334","9783662544341"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-54434-1_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"19 March 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Uppsala","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Sweden","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 April 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2017a","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.etaps.org\/index.php\/2017\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}