{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,19]],"date-time":"2026-02-19T03:21:25Z","timestamp":1771471285937,"version":"3.50.1"},"reference-count":46,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2024,6,1]],"date-time":"2024-06-01T00:00:00Z","timestamp":1717200000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2024,6,1]],"date-time":"2024-06-01T00:00:00Z","timestamp":1717200000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2024,4,18]],"date-time":"2024-04-18T00:00:00Z","timestamp":1713398400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2024,6]]},"DOI":"10.1016\/j.tcs.2024.114582","type":"journal-article","created":{"date-parts":[[2024,4,21]],"date-time":"2024-04-21T17:05:42Z","timestamp":1713719142000},"page":"114582","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":1,"special_numbering":"C","title":["Polymorphic higher-order context-free session types"],"prefix":"10.1016","volume":"1001","author":[{"given":"Diana","family":"Costa","sequence":"first","affiliation":[]},{"given":"Andreia","family":"Mordido","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5474-3614","authenticated-orcid":false,"given":"Diogo","family":"Po\u00e7as","sequence":"additional","affiliation":[]},{"given":"Vasco T.","family":"Vasconcelos","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"issue":"Part","key":"10.1016\/j.tcs.2024.114582_br0010","article-title":"Polymorphic lambda calculus with context-free session types","volume":"289","author":"Almeida","year":"2022","journal-title":"Inf. Comput."},{"key":"10.1016\/j.tcs.2024.114582_br0020","author":"Almeida"},{"key":"10.1016\/j.tcs.2024.114582_br0030","series-title":"PLACES","first-page":"12","article-title":"FreeST: context-free session types in a functional language","volume":"vol. 291","author":"Almeida","year":"2019"},{"key":"10.1016\/j.tcs.2024.114582_br0040","series-title":"TACAS","first-page":"39","article-title":"Deciding the bisimilarity of context-free session types","volume":"vol. 12079","author":"Almeida","year":"2020"},{"key":"10.1016\/j.tcs.2024.114582_br0050","series-title":"PARLE","first-page":"94","article-title":"Decidability of bisimulation equivalence for processes generating context-free languages","volume":"vol. 259","author":"Baeten","year":"1987"},{"issue":"3","key":"10.1016\/j.tcs.2024.114582_br0060","doi-asserted-by":"crossref","first-page":"653","DOI":"10.1145\/174130.174141","article-title":"Decidability of bisimulation equivalence for processes generating context-free languages","volume":"40","author":"Baeten","year":"1993","journal-title":"J. ACM"},{"key":"10.1016\/j.tcs.2024.114582_br0070","series-title":"MFCS","first-page":"423","article-title":"An elementary bisimulation decision procedure for srbitrary context-free processes","volume":"vol. 969","author":"Burkart","year":"1995"},{"key":"10.1016\/j.tcs.2024.114582_br0080","series-title":"POPL","first-page":"30","article-title":"System F-omega with equirecursive types for datatype-generic programming","author":"Cai","year":"2016"},{"key":"10.1016\/j.tcs.2024.114582_br0090","series-title":"ESOP","first-page":"330","article-title":"Behavioral polymorphism and parametricity in session-based communication","volume":"vol. 7792","author":"Caires","year":"2013"},{"issue":"1","key":"10.1016\/j.tcs.2024.114582_br0100","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1016\/0890-5401(91)90020-3","article-title":"Type inference with recursive types: syntax and semantics","volume":"92","author":"Cardone","year":"1991","journal-title":"Inf. Comput."},{"issue":"2","key":"10.1016\/j.tcs.2024.114582_br0110","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1006\/inco.1995.1129","article-title":"Bisimulation equivalence is decidable for all context-free processes","volume":"121","author":"Christensen","year":"1995","journal-title":"Inf. Comput."},{"key":"10.1016\/j.tcs.2024.114582_br0120","first-page":"24","article-title":"Higher-order context-free session types in system F","volume":"vol. 356","author":"Costa","year":"2022"},{"key":"10.1016\/j.tcs.2024.114582_br0130","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0304-3975(83)90059-2","article-title":"Fundamental properties of infinite trees","volume":"25","author":"Courcelle","year":"1983","journal-title":"Theor. Comput. Sci."},{"issue":"4","key":"10.1016\/j.tcs.2024.114582_br0140","doi-asserted-by":"crossref","first-page":"548","DOI":"10.2307\/2182503","article-title":"Combinatory logic, volume I","volume":"68","author":"Curry","year":"1959","journal-title":"Philos. Rev."},{"key":"10.1016\/j.tcs.2024.114582_br0150","first-page":"27","article-title":"Recursive session types revisited","volume":"vol. 162","author":"Dardha","year":"2014"},{"key":"10.1016\/j.tcs.2024.114582_br0160","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/j.ic.2017.06.002","article-title":"Session types revisited","volume":"256","author":"Dardha","year":"2017","journal-title":"Inf. Comput."},{"key":"10.1016\/j.tcs.2024.114582_br0170","series-title":"ESOP","first-page":"178","article-title":"Nested session types","volume":"vol. 12648","author":"Das","year":"2021"},{"key":"10.1016\/j.tcs.2024.114582_br0180","author":"Das"},{"key":"10.1016\/j.tcs.2024.114582_br0190","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","article-title":"Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem","volume":"75","author":"Govert De Bruijn","year":"1972","journal-title":"Indag. Math."},{"key":"10.1016\/j.tcs.2024.114582_br0200","series-title":"ICFP","first-page":"150","article-title":"Numbering matters: first-order canonical forms for second-order recursive types","author":"Gauthier","year":"2004"},{"issue":"5","key":"10.1016\/j.tcs.2024.114582_br0210","doi-asserted-by":"crossref","first-page":"895","DOI":"10.1017\/S0960129508006944","article-title":"Bounded polymorphism in session types","volume":"18","author":"Gay","year":"2008","journal-title":"Math. Struct. Comput. Sci."},{"issue":"2\u20133","key":"10.1016\/j.tcs.2024.114582_br0220","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/s00236-005-0177-z","article-title":"Subtyping for session types in the pi calculus","volume":"42","author":"Gay","year":"2005","journal-title":"Acta Inform."},{"key":"10.1016\/j.tcs.2024.114582_br0230","author":"Gay Diogo Po\u00e7as"},{"issue":"1","key":"10.1016\/j.tcs.2024.114582_br0240","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1145\/321250.321254","article-title":"A new normal-form theorem for context-free phrase structure grammars","volume":"12","author":"Greibach","year":"1965","journal-title":"J. ACM"},{"key":"10.1016\/j.tcs.2024.114582_br0250","series-title":"Polarized substructural session types","author":"Griffith","year":"2016"},{"issue":"1&2","key":"10.1016\/j.tcs.2024.114582_br0260","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1016\/0304-3975(95)00064-X","article-title":"A polynomial algorithm for deciding bisimilarity of normed context-free processes","volume":"158","author":"Hirshfeld","year":"1996","journal-title":"Theor. Comput. Sci."},{"key":"10.1016\/j.tcs.2024.114582_br0270","series-title":"CONCUR","first-page":"509","article-title":"Types for dyadic interaction","volume":"vol. 715","author":"Honda","year":"1993"},{"key":"10.1016\/j.tcs.2024.114582_br0280","series-title":"ESOP","first-page":"122","article-title":"Language primitives and type discipline for structured communication-based programming","volume":"vol. 1381","author":"Honda","year":"1998"},{"issue":"1","key":"10.1016\/j.tcs.2024.114582_br0290","article-title":"Bisimilarity on basic process algebra is in 2-ExpTime (an explicit proof)","volume":"9","author":"Jan\u010dar","year":"2012","journal-title":"Log. Methods Comput. Sci."},{"issue":"3","key":"10.1016\/j.tcs.2024.114582_br0300","first-page":"18:1","article-title":"Session coalgebras: a coalgebraic view on regular and context-free session types","volume":"44","author":"Keizer Henning Basold","year":"2022","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"4","key":"10.1016\/j.tcs.2024.114582_br0310","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/j.ipl.2012.12.004","article-title":"BPA bisimilarity is EXPTIME-hard","volume":"113","author":"Kiefer","year":"2013","journal-title":"Inf. Process. Lett."},{"key":"10.1016\/j.tcs.2024.114582_br0320","series-title":"SWAT","first-page":"36","article-title":"Simple deterministic languages","author":"Korenjak","year":"1966"},{"key":"10.1016\/j.tcs.2024.114582_br0330","series-title":"Lambda calculus models of programming languages","author":"Morris","year":"1968"},{"key":"10.1016\/j.tcs.2024.114582_br0340","series-title":"ESOP","first-page":"804","article-title":"Context-free session type inference","volume":"vol. 10201","author":"Padovani","year":"2017"},{"issue":"2","key":"10.1016\/j.tcs.2024.114582_br0350","doi-asserted-by":"crossref","first-page":"9:1","DOI":"10.1145\/3229062","article-title":"Context-free session type inference","volume":"41","author":"Padovani","year":"2019","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10.1016\/j.tcs.2024.114582_br0360","series-title":"Types and Programming Languages","author":"Pierce","year":"2002"},{"key":"10.1016\/j.tcs.2024.114582_br0370","series-title":"ESOP","first-page":"392","article-title":"System F\u03c9\u03bc with context-free session types","volume":"vol. 13990","author":"Po\u00e7as","year":"2023"},{"key":"10.1016\/j.tcs.2024.114582_br0380","series-title":"Euro-Par","first-page":"1334","article-title":"Non-regular process types","volume":"vol. 1685","author":"Puntigam","year":"1999"},{"key":"10.1016\/j.tcs.2024.114582_br0390","series-title":"Euro-Par","first-page":"554","article-title":"Behavioural types for a calculus of concurrent objects","volume":"vol. 1300","author":"Ravara","year":"1997"},{"key":"10.1016\/j.tcs.2024.114582_br0400","series-title":"An Introduction to Bisimulation and Coinduction","author":"Sangiorgi","year":"2014"},{"key":"10.1016\/j.tcs.2024.114582_br0410","series-title":"CONCUR","first-page":"11:1","article-title":"Subtyping context-free session types","volume":"vol. 279","author":"Silva","year":"2023"},{"key":"10.1016\/j.tcs.2024.114582_br0420","series-title":"SC","first-page":"99","article-title":"A model of components with non-regular protocols","volume":"vol. 3628","author":"S\u00fcdholt","year":"2005"},{"key":"10.1016\/j.tcs.2024.114582_br0430","series-title":"PARLE","first-page":"398","article-title":"An interaction-based language and its typing system","volume":"vol. 817","author":"Takeuchi","year":"1994"},{"key":"10.1016\/j.tcs.2024.114582_br0440","series-title":"ICFP","first-page":"462","article-title":"Context-free session types","author":"Thiemann","year":"2016"},{"issue":"2","key":"10.1016\/j.tcs.2024.114582_br0450","doi-asserted-by":"crossref","DOI":"10.1145\/3457884","article-title":"On polymorphic sessions and functions: a tale of two (fully abstract) encodings","volume":"43","author":"Toninho","year":"2021","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10.1016\/j.tcs.2024.114582_br0460","series-title":"ICFP","first-page":"273","article-title":"Propositions as sessions","author":"Wadler","year":"2012"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S030439752400197X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S030439752400197X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2024,5,6]],"date-time":"2024-05-06T06:49:14Z","timestamp":1714978154000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S030439752400197X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6]]},"references-count":46,"alternative-id":["S030439752400197X"],"URL":"https:\/\/doi.org\/10.1016\/j.tcs.2024.114582","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2024,6]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Polymorphic higher-order context-free session types","name":"articletitle","label":"Article Title"},{"value":"Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.tcs.2024.114582","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2024 The Author(s). Published by Elsevier B.V.","name":"copyright","label":"Copyright"}],"article-number":"114582"}}