{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:57:21Z","timestamp":1776891441173,"version":"3.51.2"},"reference-count":38,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2016,12,21]],"date-time":"2016-12-21T00:00:00Z","timestamp":1482278400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2017]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Inspired by the continuation-passing encoding of binary sessions, we describe a simple approach to embed a hybrid form of session type checking into any programming language that supports parametric polymorphism. The approach combines static protocol analysis with dynamic linearity checks. To demonstrate the effectiveness of the technique, we implement a well-integrated\n                    <jats:monospace>OCaml<\/jats:monospace>\n                    module for session communications. For free,\n                    <jats:monospace>OCaml<\/jats:monospace>\n                    provides us with equirecursive session types, parametric behavioural polymorphism, complete session type inference, and session subtyping.\n                  <\/jats:p>","DOI":"10.1017\/s0956796816000289","type":"journal-article","created":{"date-parts":[[2016,12,21]],"date-time":"2016-12-21T04:31:59Z","timestamp":1482294719000},"source":"Crossref","is-referenced-by-count":44,"title":["A simple library implementation of binary sessions"],"prefix":"10.46298","volume":"27","author":[{"given":"LUCA","family":"PADOVANI","sequence":"first","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2016,12,21]]},"reference":[{"key":"S0956796816000289_ref31","volume-title":"Session Types in Haskell: Updating Message Passing for the 21st Century","author":"Sackman","year":"2008"},{"key":"S0956796816000289_ref9","unstructured":"Demangeon R. & Honda R. (2011) Full abstraction in a subtyped pi-calculus with linear types. In Proceedings of CONCUR'11, LNCS, vol. 6901. Springer, Germany, pp. 280\u2013296."},{"key":"S0956796816000289_ref15","doi-asserted-by":"crossref","unstructured":"Honda K. , Vasconcelos V. T. & Kubo M. (1998) Language primitives and type disciplines for structured communication-based programming. In Proceedings of ESOP'98, LNCS, vol. 1381. Springer, Germany, pp. 122\u2013138.","DOI":"10.1007\/BFb0053567"},{"key":"S0956796816000289_ref17","unstructured":"Hu R. & Yoshida N. (2016) Hybrid session verification through endpoint API generation. In Proceedings of FASE'16, LNCS, vol. 9633. Springer, Germany, pp. 401\u2013418."},{"key":"S0956796816000289_ref16","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328472"},{"key":"S0956796816000289_ref22","doi-asserted-by":"publisher","DOI":"10.1145\/330249.330251"},{"key":"S0956796816000289_ref28","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":"Math. Struct. Comput. Sci."},{"key":"S0956796816000289_ref4","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(1:17)2012"},{"key":"S0956796816000289_ref23","unstructured":"Leroy X. , Doligez D. , Frisch A. , Garrigue J. , R\u00e9my D. & Vouillon J. (2014) The Objective Caml System. Available at http:\/\/caml.inria.fr\/pub\/docs\/manual-ocaml\/. Last accessed in November 2016."},{"key":"S0956796816000289_ref35","unstructured":"Tov J. A. & Pucella R. (2011) Practical affine types. In Proceedings of POPL'11. ACM, USA, pp. 447\u2013458."},{"key":"S0956796816000289_ref1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000031"},{"key":"S0956796816000289_ref2","doi-asserted-by":"crossref","unstructured":"Bartoletti M. , Cimoli T. , Murgia M. , Podda A.-S. & Pompianu L. (2015) Compliance and subtyping in timed session types. In Proceedings of FORTE'15, LNCS, vol. 9039. Springer, Germany, pp. 161\u2013177.","DOI":"10.1007\/978-3-319-19195-9_11"},{"key":"S0956796816000289_ref32","unstructured":"Scalas A. & Yoshida N. (2016) Lightweight session programming in scala. In Proceedings of ECOOP'16, LIPIcs, Germany, vol. 56. Schloss Dagstuhl, pp. 21:1\u201321:28."},{"key":"S0956796816000289_ref7","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90059-2"},{"key":"S0956796816000289_ref34","unstructured":"Tov J. A. & Pucella R. (2010) Stateful contracts for affine types. In Proceedings of ESOP'10, LNCS, vol. 6012. Springer, Germany, pp. 550\u2013569."},{"key":"S0956796816000289_ref37","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681400001X"},{"key":"S0956796816000289_ref26","volume-title":"A Simple Library Implementation of Binary Sessions","author":"Padovani","year":"2015"},{"key":"S0956796816000289_ref18","unstructured":"Hunt G. , Larus J. R. , Abadi M. , Aiken M. , Barham P. , F\u00e4hndrich M. , Hawblitzel C. , Hodson O. , Levi S. , Murphy N. , Steensgaard B. , Tarditi D. , Wobber T. & Zill B. (2005) An Overview of the Singularity Project. Technical Report MSR-TR-2005-135, Microsoft Research."},{"key":"S0956796816000289_ref33","unstructured":"Tov J. A. (2012) Practical Programming with Substructural Types. PhD thesis, Northeastern University."},{"key":"S0956796816000289_ref6","unstructured":"Chen T.-C. , Bocchi L. , Deni\u00e9lou P.-M. , Honda K. & Yoshida N. (2011) Asynchronous distributed monitoring for multiparty session enforcement. In Proceedings of TGC'11, LNCS, vol. 7173. Springer, Germany, pp. 25\u201345."},{"key":"S0956796816000289_ref3","doi-asserted-by":"crossref","unstructured":"Bocchi L. , Chen T.-C. , Demangeon R. , Honda K. & Yoshida N. (2013) Monitoring networks through multiparty session types. In Proceedings of FMOODS\/FORTE'13, LNCS, vol. 7892. Springer, Germany, pp. 50\u201365.","DOI":"10.1007\/978-3-642-38592-6_5"},{"key":"S0956796816000289_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-014-0218-8"},{"key":"S0956796816000289_ref13","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990268"},{"key":"S0956796816000289_ref8","doi-asserted-by":"publisher","DOI":"10.1145\/2370776.2370794"},{"key":"S0956796816000289_ref14","doi-asserted-by":"crossref","unstructured":"Honda K. (1993) Types for dyadic interaction. In Proceedings of CONCUR'93, LNCS, vol. 715. Springer, Germany, pp. 509\u2013523.","DOI":"10.1007\/3-540-57208-2_35"},{"key":"S0956796816000289_ref24","unstructured":"Neubauer M. & Thiemann P. (2004) An implementation of session types. In Proceedings of PADL'04, LNCS, vol. 3057. Springer, Germany, pp. 56\u201370."},{"key":"S0956796816000289_ref21","doi-asserted-by":"crossref","unstructured":"Kobayashi N. (2002) Type systems for concurrent programs. In Proceedings of the 10th Anniversary Colloquium of UNU\/IIST, LNCS, vol. 2757. Springer, Germany, pp. 439\u2013453. Extended version available at http:\/\/www.kb.ecei.tohoku.ac.jp\/koba\/papers\/tutorial-type-extended.pdf.","DOI":"10.1007\/978-3-540-40007-3_26"},{"key":"S0956796816000289_ref25","doi-asserted-by":"crossref","unstructured":"Padovani L. (2014) Deadlock and lock freedom in the linear \u03c0-calculus. In Proceedings of CSL-LICS'14. ACM, USA, pp. 72:1\u201372:10. Extended version available at http:\/\/hal.archives-ouvertes.fr\/hal-00932356v2\/.","DOI":"10.1145\/2603088.2603116"},{"key":"S0956796816000289_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-005-0177-z"},{"key":"S0956796816000289_ref20","unstructured":"Jane Street Developers. (August 2016) Core library documentation. Available at https:\/\/ocaml.janestreet.com\/ocaml-core\/latest\/doc\/core\/. Last accessed in November 2016."},{"key":"S0956796816000289_ref19","unstructured":"Imai K. , Yuen S. & Agusa K. (2010) Session type inference in Haskell. In Proceedings of PLACES'10, EPTCS 69, Open Publishing Association, pp. 74\u201391."},{"key":"S0956796816000289_ref38","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"S0956796816000289_ref27","volume-title":"Context-Free Session Type Inference","author":"Padovani","year":"2016"},{"key":"S0956796816000289_ref11","unstructured":"Garrigue J. (1998) Programming with polymorphic variants. In Informal Proceedings of ACM SIGPLAN Workshop on ML. Available at https:\/\/caml.inria.fr\/pub\/papers\/garrigue-polymorphic_variants-ml98.pdf, last accessed November 2016."},{"key":"S0956796816000289_ref5","unstructured":"Caires L. & P\u00e9rez J. A. (2016) Multiparty session types within a canonical binary theory, and beyond. In Proceedings of FORTE'16, LNCS, vol. 9688. Springer, Germany, pp. 74\u201395."},{"key":"S0956796816000289_ref29","doi-asserted-by":"publisher","DOI":"10.1145\/1411286.1411290"},{"key":"S0956796816000289_ref36","unstructured":"Vasconcelos V. T. & Thiemann P. (2016) Context-free session types. In Proceedings of ICFP'16. ACM, USA, pp. 462\u2013475."},{"key":"S0956796816000289_ref30","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511574962"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796816000289","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:19:53Z","timestamp":1776889193000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796816000289\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,12,21]]},"references-count":38,"alternative-id":["S0956796816000289"],"URL":"https:\/\/doi.org\/10.1017\/s0956796816000289","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,12,21]]},"article-number":"e4"}}