{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,8]],"date-time":"2025-11-08T17:42:22Z","timestamp":1762623742910,"version":"3.37.3"},"reference-count":23,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2016,7,1]],"date-time":"2016-07-01T00:00:00Z","timestamp":1467331200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"ICT COST Action","award":["IC1201 BETTY"],"award-info":[{"award-number":["IC1201 BETTY"]}]},{"DOI":"10.13039\/501100003407","name":"MIUR","doi-asserted-by":"crossref","award":["Project CINA Prot. 2010LHT4KM"],"award-info":[{"award-number":["Project CINA Prot. 2010LHT4KM"]}],"id":[{"id":"10.13039\/501100003407","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Torino University\/Compagnia San Paolo","award":["Project SALT"],"award-info":[{"award-number":["Project SALT"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2016,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            In the setting of\n            <jats:italic>session behaviours<\/jats:italic>\n            , we study an extension of the concept of compliance when a disciplined form of backtracking and of output skipping is present. After adding checkpoints to the syntax of session behaviours, we formalise the operational semantics via an LTS, and define natural notions of\n            <jats:italic>checkpoint compliance<\/jats:italic>\n            and\n            <jats:italic>sub-behaviour<\/jats:italic>\n            , which we prove to be both decidable. Then we extend the operational semantics with\n            <jats:italic>skips<\/jats:italic>\n            and we show the decidability of the obtained compliance.\n          <\/jats:p>","DOI":"10.1007\/s00165-016-0358-2","type":"journal-article","created":{"date-parts":[[2016,2,24]],"date-time":"2016-02-24T12:20:45Z","timestamp":1456316445000},"page":"697-722","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Reversible client\/server interactions"],"prefix":"10.1145","volume":"28","author":[{"given":"Franco","family":"Barbanera","sequence":"first","affiliation":[{"name":"Dipartimento di Matematica e Informatica, Universit\u00e0 di Catania, Viale A. Doria 6, 95125, Catania, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mariangiola","family":"Dezani-Ciancaglini","sequence":"additional","affiliation":[{"name":"Universit\u00e0 di Torino, Torino, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ugo","family":"de\u2019Liguoro","sequence":"additional","affiliation":[{"name":"Universit\u00e0 di Torino, Torino, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Barbanera F Dezani-Ciancaglini M de\u2019 Liguoro U (2014) Compliance for reversible client\/server interactions. In BEAT 162 of EPTCS Open Publishing Association pp 35\u201342","DOI":"10.4204\/EPTCS.162.5"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Barbanera F de\u2019 Liguoro U (2014) Loosening the notions of compliance and sub-behaviour in client\/server systems. In ICE 166 of EPTCS Open Publishing Association pp 94\u2013110","DOI":"10.4204\/EPTCS.166.10"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1017\/S096012951400005X"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Barbanera F Dezani-Ciancaglini M Lanese I de\u2019 Liguoro U (2016) Retractable contracts. In PLACES 203 of EPTCS Open Publishing Association pp 61\u201372","DOI":"10.4204\/EPTCS.203.5"},{"issue":"4","key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","first-page":"309","DOI":"10.3233\/FI-1998-33401","article-title":"Coinductive axiomatization of recursive type equality and subtyping","volume":"33","author":"Brandt M","year":"1998","journal-title":"Fundamenta Informaticae"},{"key":"e_1_2_1_2_6_2","unstructured":"Bernardi G Hennessy M (2015) Modelling session types using contracts. Math Struct Comp Sci FirstView (9):1\u201351"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Carpineti S Castagna G Laneve C Padovani L (2006) A formal account of contracts for Web Services. In WS-FM number 4184 in LNCS. Springer pp 148\u2013162","DOI":"10.1007\/11841197_10"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Castagna G Gesbert N Padovani L (2009) A theory of contracts for web services. ACM Trans Program Lang Systems 31(5):19:1\u201319:61","DOI":"10.1145\/1538917.1538920"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Danos V Krivine J (2004) Reversible communicating systems. In CONCUR volume 3170 of LNCS . Springer pp 292\u2013307","DOI":"10.1007\/978-3-540-28644-8_19"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"de Vries E Koutavas V Hennessy M (2010) Communicating transactions - (extended abstract). In CONCUR volume 6269 of LNCS . Springer pp 569\u2013583","DOI":"10.1007\/978-3-642-15375-4_39"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"de Vries E Koutavas V Hennessy M (2010) Liveness of communicating transactions\u2014(extended abstract). In APLAS volume 6461 of LNCS . Springer pp 392\u2013407","DOI":"10.1007\/978-3-642-17164-2_27"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Honda K Vasconcelos VT Kubo M (1998) Language primitives and type disciplines for structured communication-based programming. In ESOP volume 1381 of LNCS . Springer pp 22\u2013138","DOI":"10.1007\/BFb0053567"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Honda K Yoshida N Carbone M (2008) Multiparty asynchronous session types. In POPL . ACM Press pp 273\u2013284","DOI":"10.1145\/1328897.1328472"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Koutavas V Spaccasassi C Hennessy M (2014) Bisimulations for communicating transactions\u2014(extended abstract). In FOSSACS volume 8412 of LNCS . Springer pp 320\u2013334","DOI":"10.1007\/978-3-642-54830-7_21"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Lanese I Mezzina CA Stefani J-B (2010) Reversing higher-order pi. In CONCUR volume 6269 of LNCS . Springer pp 478\u2013493","DOI":"10.1007\/978-3-642-15375-4_33"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Lanese I Mezzina CA Schmitt A Stefani J-B (2011) Controlling reversibility in higher-order pi. In CONCUR volume 6901 of LNCS . Springer pp 297\u2013311","DOI":"10.1007\/978-3-642-23217-6_20"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Laneve C Padovani L (2008) The pairing of contracts and session types. In Concurrency Graphs and Models 5065 of LNCS . Springer pp 681\u2013700","DOI":"10.1007\/978-3-540-68679-8_42"},{"volume-title":"Communication and concurrency","year":"1989","author":"Milner R","key":"e_1_2_1_2_18_2"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.05.002"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950007002X"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2006.11.002"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Tiezzi F Yoshida N (2014) Towards reversible sessions. In PLACES volume 155 of EPTCS . Open Publishing Association pp 17\u201324","DOI":"10.4204\/EPTCS.155.3"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2015.03.004"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0358-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-016-0358-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-016-0358-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:07:04Z","timestamp":1641485224000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-016-0358-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,7]]},"references-count":23,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2016,7]]}},"alternative-id":["10.1007\/s00165-016-0358-2"],"URL":"https:\/\/doi.org\/10.1007\/s00165-016-0358-2","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2016,7]]}}}