{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,3]],"date-time":"2026-06-03T07:35:39Z","timestamp":1780472139036,"version":"3.54.1"},"reference-count":44,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2014,11,10]],"date-time":"2014-11-10T00:00:00Z","timestamp":1415577600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2016,2]]},"abstract":"<jats:p>Event-driven programming is one of the major paradigms in concurrent and communication-based programming, where events are typically detected as the arrival of messages on asynchronous channels. Unfortunately, the flexibility and performance of traditional event-driven programming come at the cost of more complex programs: low-level APIs and the obfuscation of event-driven control flow make programs difficult to read, write and verify.<\/jats:p><jats:p>This paper introduces a \u03c0-calculus with session types that models<jats:italic>event-driven session programming<\/jats:italic>(called ESP) and studies its behavioural theory. The main characteristics of the ESP model are asynchronous, order-preserving message passing, non-blocking detection of event\/message arrivals and dynamic inspection of session types. Session types offer formal safety guarantees, such as communication and event handling safety, and programmatic benefits that overcome problems with existing event-driven programming languages and techniques. The new typed bisimulation theory developed for the ESP model is distinct from standard synchronous or asynchronous bisimulation, capturing the semantic nature of eventful session-based processes. The bisimilarity coincides with reduction-closed barbed congruence.<\/jats:p><jats:p>We demonstrate the features and benefits of ESP and the behavioural theory through two key use cases. First, we examine an encoding and the semantic behaviour of the event selector, a central component of general event-driven systems, providing core results for verifying type-safe event-driven applications. Second, we examine the Lauer\u2013Needham duality, building on the selector encoding and bisimulation theory to prove that a systematic transformation from multithreaded to event-driven session processes is type- and semantics-preserving.<\/jats:p>","DOI":"10.1017\/s096012951400019x","type":"journal-article","created":{"date-parts":[[2014,11,10]],"date-time":"2014-11-10T12:24:27Z","timestamp":1415622267000},"page":"303-364","source":"Crossref","is-referenced-by-count":15,"title":["On asynchronous eventful session semantics"],"prefix":"10.1017","volume":"26","author":[{"given":"DIMITRIOS","family":"KOUZAPAS","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"NOBUKO","family":"YOSHIDA","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"RAYMOND","family":"HU","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"KOHEI","family":"HONDA","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2014,11,10]]},"reference":[{"key":"S096012951400019X_ref27","doi-asserted-by":"publisher","DOI":"10.1145\/850657.850658"},{"key":"S096012951400019X_ref14","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511611063"},{"key":"S096012951400019X_ref33","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"S096012951400019X_ref32","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10235-3"},{"key":"S096012951400019X_ref29","doi-asserted-by":"publisher","DOI":"10.1145\/1273442.1250756"},{"key":"S096012951400019X_ref34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02273-9_16"},{"key":"S096012951400019X_ref7","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00227-3"},{"key":"S096012951400019X_ref23","unstructured":"Kouzapas D. (2009) A Session Type Discipline for Event Driven Programming Models, Master's thesis, Imperial College London. Available at http:\/\/www.doc.ic.ac.uk\/teaching\/distinguished-projects\/2010\/d.kouzapas.pdf."},{"key":"S096012951400019X_ref20","unstructured":"Hu R. (2011) SJ homepage. Available at http:\/\/www.doc.ic.ac.uk\/~rhu\/sessionj.html."},{"key":"S096012951400019X_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04081-8_15"},{"key":"S096012951400019X_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_16"},{"key":"S096012951400019X_ref39","unstructured":"SJ (2010) SJ homepage. Available at http:\/\/www.doc.ic.ac.uk\/~rhu\/sessionj.html."},{"key":"S096012951400019X_ref37","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1017\/S096012950007002X","article-title":"Typing and subtyping for mobile processes","volume":"6","author":"Pierce","year":"1996","journal-title":"Mathematical Structures in Computer Science"},{"key":"S096012951400019X_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72952-5_1"},{"key":"S096012951400019X_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0057019"},{"key":"S096012951400019X_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_16"},{"key":"S096012951400019X_ref26","unstructured":"Krohn M. , Kohler E. and Kaashoek M. F. (2007) Events can make sense. In: Annual Technical Conference'07, USENIX Association 1\u201314."},{"key":"S096012951400019X_ref9","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.09.010"},{"key":"S096012951400019X_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_27"},{"key":"S096012951400019X_ref13","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990268"},{"key":"S096012951400019X_ref25","unstructured":"Krohn M. (2004) Building secure high-performance web services with OKWS. In: ATEC'04, USENIX Association 15\u201315."},{"key":"S096012951400019X_ref3","unstructured":"Adya A. , Howell J. , Theimer M. , Bolosky W. J. and Douceur J. R. (2002) Cooperative task management without manual stack management or, event-driven programming is not the opposite of threaded programming. In: Proceedings of the 2002 Usenix ATC 289\u2013302."},{"key":"S096012951400019X_ref1","doi-asserted-by":"publisher","DOI":"10.1145\/103135.103138"},{"key":"S096012951400019X_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70592-5_22"},{"key":"S096012951400019X_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21461-5_15"},{"key":"S096012951400019X_ref38","volume-title":"Types and Programming Languages","author":"Pierce","year":"2002"},{"key":"S096012951400019X_ref43","doi-asserted-by":"publisher","DOI":"10.1145\/945445.945471"},{"key":"S096012951400019X_ref19","first-page":"273","volume-title":"Principles of programming languages'08","author":"Honda","year":"2008"},{"key":"S096012951400019X_ref42","unstructured":"von Behren R. , Condit J. and Brewer E. (2003a) Why events are a bad idea (for high-concurrency servers) In: Proceedings of HOTOS'03, USENIX Association 4\u20134."},{"key":"S096012951400019X_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85361-9_33"},{"key":"S096012951400019X_ref44","doi-asserted-by":"publisher","DOI":"10.1145\/502034.502057"},{"key":"S096012951400019X_ref2","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680000126X"},{"key":"S096012951400019X_ref4","doi-asserted-by":"publisher","DOI":"10.1145\/306225.306234"},{"key":"S096012951400019X_ref30","unstructured":"Lowe G. (2009) Extending CSP with tests for availability. In: Proceedings of Communicating Process Architectures (CPA 2009) 325\u2013347."},{"key":"S096012951400019X_ref16","first-page":"22","article-title":"Language primitives and type disciplines for structured communication-based programming","volume":"1381","author":"Honda","year":"1998","journal-title":"Springer Lecture Notes in Computer Science"},{"key":"S096012951400019X_ref28","unstructured":"Lea D. (2003) Scalable IO in Java. Available at http:\/\/gee.cs.oswego.edu\/dl\/cpjslides\/nio.pdf."},{"key":"S096012951400019X_ref31","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.41.7"},{"key":"S096012951400019X_ref41","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58184-7_118"},{"key":"S096012951400019X_ref40","unstructured":"Sun Microsystems Inc. (2011) New IO APIs. Available at http:\/\/java.sun.com\/j2se\/1.4.2\/docs\/guide\/nio\/index.html."},{"key":"S096012951400019X_ref17","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00074-7"},{"key":"S096012951400019X_ref11","first-page":"219","volume-title":"Principles and Practice of Declarative Programming'09","author":"Castagna","year":"2009"},{"key":"S096012951400019X_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68679-8_29"},{"key":"S096012951400019X_ref18","doi-asserted-by":"publisher","DOI":"10.1145\/1286821.1286822"},{"key":"S096012951400019X_ref36","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63165-8_188"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S096012951400019X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,17]],"date-time":"2019-08-17T01:43:02Z","timestamp":1566006182000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S096012951400019X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,10]]},"references-count":44,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2016,2]]}},"alternative-id":["S096012951400019X"],"URL":"https:\/\/doi.org\/10.1017\/s096012951400019x","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,11,10]]}}}