{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,10]],"date-time":"2026-03-10T08:12:26Z","timestamp":1773130346355,"version":"3.50.1"},"reference-count":59,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T00:00:00Z","timestamp":1775001600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T00:00:00Z","timestamp":1775001600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2025,12,9]],"date-time":"2025-12-09T00:00:00Z","timestamp":1765238400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001871","name":"Foundation for Science and Technology","doi-asserted-by":"publisher","award":["2023.13752"],"award-info":[{"award-number":["2023.13752"]}],"id":[{"id":"10.13039\/501100001871","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2026,4]]},"DOI":"10.1016\/j.tcs.2025.115705","type":"journal-article","created":{"date-parts":[[2025,12,18]],"date-time":"2025-12-18T00:23:13Z","timestamp":1766017393000},"page":"115705","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"C","title":["Subtyping context-free session types"],"prefix":"10.1016","volume":"1069","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-7051-6116","authenticated-orcid":false,"given":"Gil","family":"Silva","sequence":"first","affiliation":[]},{"given":"Andreia","family":"Mordido","sequence":"additional","affiliation":[]},{"given":"Vasco T.","family":"Vasconcelos","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.tcs.2025.115705_bib0001","series-title":"CONCUR 2023, Proceedings","first-page":"11:1","article-title":"Subtyping context-free session types","volume":"279","author":"Silva","year":"2023"},{"key":"10.1016\/j.tcs.2025.115705_bib0002","series-title":"CONCUR \u201993, Proceedings","first-page":"509","article-title":"Types for dyadic interaction","volume":"715","author":"Honda","year":"1993"},{"key":"10.1016\/j.tcs.2025.115705_bib0003","series-title":"ESOP\u201998, Proceedings","first-page":"122","article-title":"Language primitives and type discipline for structured communication-based programming","volume":"1381","author":"Honda","year":"1998"},{"key":"10.1016\/j.tcs.2025.115705_bib0004","series-title":"PARLE \u201994, Proceedings","first-page":"398","article-title":"An interaction-based language and its typing system","volume":"817","author":"Takeuchi","year":"1994"},{"key":"10.1016\/j.tcs.2025.115705_bib0005","series-title":"ICFP 2016, Proceedings","first-page":"462","article-title":"Context-free session types","author":"Thiemann","year":"2016"},{"issue":"2-3","key":"10.1016\/j.tcs.2025.115705_bib0006","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.2025.115705_bib0007","series-title":"OOPSLA 1987, Addendum to Proceedings, USA, October 4\u20138, 1987","first-page":"17","article-title":"Keynote address - data abstraction and hierarchy","author":"Liskov","year":"1987"},{"issue":"5","key":"10.1016\/j.tcs.2025.115705_bib0008","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":"10.1016\/j.tcs.2025.115705_bib0009","unstructured":"Amazon Ion, 2024, (https:\/\/amazon-ion.github.io). Accessed: October 2024."},{"issue":"2","key":"10.1016\/j.tcs.2025.115705_bib0010","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."},{"issue":"4","key":"10.1016\/j.tcs.2025.115705_bib0011","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1016\/0304-3975(76)90074-8","article-title":"The inclusion problem for simple languages","volume":"1","author":"Friedman","year":"1976","journal-title":"Theor. Comput. Sci."},{"key":"10.1016\/j.tcs.2025.115705_bib0012","series-title":"CONCUR 2010, Proceedings","first-page":"71","article-title":"Learning i\/o automata","volume":"6269","author":"Aarts","year":"2010"},{"key":"10.1016\/j.tcs.2025.115705_bib0013","series-title":"TACAS@ETAPS 2020, Proceedings","first-page":"39","article-title":"Deciding the bisimilarity of context-free session types","volume":"12079","author":"Almeida","year":"2020"},{"key":"10.1016\/j.tcs.2025.115705_bib0014","series-title":"7th Annual Symposium on Switching and Automata Theory, Berkeley, California, USA, October 23\u201325, 1966","first-page":"36","article-title":"Simple deterministic languages","author":"Korenjak","year":"1966"},{"issue":"Part","key":"10.1016\/j.tcs.2025.115705_bib0015","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.2025.115705_bib0016","doi-asserted-by":"crossref","DOI":"10.1016\/j.tcs.2024.114582","article-title":"Polymorphic higher-order context-free session types","volume":"1001","author":"Costa","year":"2024","journal-title":"Theor. Comput. Sci."},{"key":"10.1016\/j.tcs.2025.115705_bib0017","series-title":"ESOP@ETAPS 2023, Proceedings","first-page":"392","article-title":"System f\u03c9\u03bc with context-free session types","volume":"13990","author":"Po\u00e7as","year":"2023"},{"key":"10.1016\/j.tcs.2025.115705_bib0018","series-title":"Technical Report","article-title":"Subtyping between Standard and Linear Function Types","author":"Gay","year":"2006"},{"issue":"1","key":"10.1016\/j.tcs.2025.115705_bib0019","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1017\/S0956796809990268","article-title":"Linear type theory for asynchronous session types","volume":"20","author":"Gay","year":"2010","journal-title":"J. Funct. Program."},{"key":"10.1016\/j.tcs.2025.115705_bib0020","series-title":"TLDI 2010, Proceedings","first-page":"77","article-title":"Lightweight linear types in system F\u2218","author":"Mazurak","year":"2010"},{"issue":"2","key":"10.1016\/j.tcs.2025.115705_bib0021","doi-asserted-by":"crossref","first-page":"354","DOI":"10.1006\/inco.1994.1101","article-title":"Undecidable equivalences for basic process algebra","volume":"115","author":"Groote","year":"1994","journal-title":"Inf. Comput."},{"key":"10.1016\/j.tcs.2025.115705_bib0022","article-title":"A Calculus of Communicating Systems","volume":"92","author":"Milner","year":"1980"},{"key":"10.1016\/j.tcs.2025.115705_bib0023","series-title":"Types and programming languages","author":"Pierce","year":"2002"},{"key":"10.1016\/j.tcs.2025.115705_bib0024","series-title":"Proceedings of the 2nd International Joint Conference on Artificial Intelligence. London, UK, September 1\u20133, 1971","first-page":"481","article-title":"An algebraic definition of simulation between programs","author":"Milner","year":"1971"},{"key":"10.1016\/j.tcs.2025.115705_bib0025","series-title":"Theor. Comput. Sci., 5th GI-Conference, Proceedings","first-page":"167","article-title":"Concurrency and automata on infinite sequences","volume":"104","author":"Park","year":"1981"},{"key":"10.1016\/j.tcs.2025.115705_bib0026","series-title":"LICS \u201988, Proceedings","first-page":"203","article-title":"A modal process logic","author":"Larsen","year":"1988"},{"key":"10.1016\/j.tcs.2025.115705_bib0027","series-title":"CONCUR \u201998, Proceedings","first-page":"163","article-title":"Alternating refinement relations","volume":"1466","author":"Alur","year":"1998"},{"key":"10.1016\/j.tcs.2025.115705_bib0028","series-title":"CALCO 2009, Proceedings","first-page":"221","article-title":"Non-strongly stable orders also define interesting simulation relations","volume":"5728","author":"F\u00e1bregas","year":"2009"},{"key":"10.1016\/j.tcs.2025.115705_bib0029","series-title":"IEEE Symposium on Logic in Computer Science 2001, Proceedings","first-page":"323","article-title":"A symbolic labelled transition system for coinductive subtyping of f\u03bc< types","author":"Jeffrey","year":"2001"},{"issue":"1","key":"10.1016\/j.tcs.2025.115705_bib0030","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.2025.115705_bib0031","series-title":"CONCUR \u201992, Proceedings","first-page":"138","article-title":"Bisimulation equivalence is decidable for all context-free processes","volume":"630","author":"Christensen","year":"1992"},{"key":"10.1016\/j.tcs.2025.115705_bib0032","series-title":"CONCUR \u201999, Proceedings","first-page":"30","article-title":"Techniques for decidability and undecidability of bisimilarity","volume":"1664","author":"Jancar","year":"1999"},{"key":"10.1016\/j.tcs.2025.115705_bib0033","series-title":"PLACES@ETAPS 2019, Proceedings","first-page":"12","article-title":"FreeST: context-free session types in a functional language","volume":"291","author":"Almeida","year":"2019"},{"key":"10.1016\/j.tcs.2025.115705_sbref0034","series-title":"FreeST, A Concurrent Programming Language with Context-Free Session Types","author":"Almeida","year":"2019"},{"key":"10.1016\/j.tcs.2025.115705_bib0035","series-title":"(ICFP) \u201900, Proceedings","first-page":"268","article-title":"Quickcheck: a lightweight tool for random testing of haskell programs","author":"Claessen","year":"2000"},{"key":"10.1016\/j.tcs.2025.115705_bib0036","series-title":"POPL 2008, Proceedings","first-page":"273","article-title":"Multiparty asynchronous session types","author":"Honda","year":"2008"},{"key":"10.1016\/j.tcs.2025.115705_bib0037","series-title":"Programming Languages and Systems - 30th European Symposium on Programming, ESOP@ETAPS 2021, Proceedings","first-page":"178","article-title":"Nested session types","volume":"12648","author":"Das","year":"2021"},{"key":"10.1016\/j.tcs.2025.115705_bib0038","article-title":"Kind inference for the freeST programming language","author":"Almeida","year":"2023","journal-title":"CoRR"},{"issue":"4","key":"10.1016\/j.tcs.2025.115705_bib0039","doi-asserted-by":"crossref","first-page":"575","DOI":"10.1145\/155183.155231","article-title":"Subtyping recursive types","volume":"15","author":"Amadio","year":"1993","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"4","key":"10.1016\/j.tcs.2025.115705_bib0040","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","year":"1998","journal-title":"Fundam. Inform."},{"key":"10.1016\/j.tcs.2025.115705_bib0041","series-title":"PPDP 2005, Proceedings","first-page":"198","article-title":"A gentle introduction to semantic subtyping","author":"Castagna","year":"2005"},{"key":"10.1016\/j.tcs.2025.115705_bib0042","first-page":"5","article-title":"Polymorphic Functions with Set-Theoretic Types: Part 1: Syntax, Semantics, and Evaluation","author":"Castagna","year":"2014"},{"key":"10.1016\/j.tcs.2025.115705_bib0043","series-title":"MPC 2010, Proceedings","first-page":"100","article-title":"Subtyping, declaratively","author":"Danielsson","year":"2010"},{"key":"10.1016\/j.tcs.2025.115705_bib0044","series-title":"Algebraic Subtyping: Distinguished Dissertation 2017","author":"Dolan","year":"2017"},{"key":"10.1016\/j.tcs.2025.115705_bib0045","series-title":"ESOP@ETAPS 2022, Proceedings","first-page":"431","article-title":"Polarized subtyping","author":"Lakhani","year":"2022"},{"key":"10.1016\/j.tcs.2025.115705_bib0046","series-title":"ESOP@ETAPS 2007, Proceedings","first-page":"2","article-title":"Structured communication-centred programming for web services","volume":"4421","author":"Carbone","year":"2007"},{"key":"10.1016\/j.tcs.2025.115705_bib0047","series-title":"A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday","first-page":"95","article-title":"Subtyping supports safe session substitution","volume":"9600","author":"Gay","year":"2016"},{"issue":"1","key":"10.1016\/j.tcs.2025.115705_bib0048","doi-asserted-by":"crossref","first-page":"4:1","DOI":"10.1145\/2994596","article-title":"On subtyping-relation completeness, with an application to iso-recursive types","volume":"39","author":"Ligatti","year":"2017","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10.1016\/j.tcs.2025.115705_bib0049","series-title":"Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming, Kent, Canterbury, United Kingdom, September 8\u201310, 2014","first-page":"135","article-title":"On the preciseness of subtyping in session types","author":"Chen","year":"2014"},{"issue":"2","key":"10.1016\/j.tcs.2025.115705_bib0050","article-title":"On the preciseness of subtyping in session types","volume":"13","author":"Chen","year":"2017","journal-title":"Log. Methods Comput. Sci."},{"key":"10.1016\/j.tcs.2025.115705_bib0051","doi-asserted-by":"crossref","first-page":"300","DOI":"10.1016\/j.ic.2017.07.010","article-title":"Undecidability of asynchronous session subtyping","volume":"256","author":"Bravetti","year":"2017","journal-title":"Inf. Comput."},{"issue":"5","key":"10.1016\/j.tcs.2025.115705_bib0052","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."},{"key":"10.1016\/j.tcs.2025.115705_bib0053","article-title":"A logical account of subtyping for session types","author":"Horne","year":"2023","journal-title":"CoRR"},{"issue":"3","key":"10.1016\/j.tcs.2025.115705_bib0054","doi-asserted-by":"crossref","first-page":"510","DOI":"10.1017\/S0960129514000243","article-title":"Modelling session types using contracts","volume":"26","author":"Bernardi","year":"2016","journal-title":"Math. Struct. Comput. Sci."},{"key":"10.1016\/j.tcs.2025.115705_bib0055","article-title":"Session-typed concurrent contracts","volume":"124","author":"Gommerstadt","year":"2022","journal-title":"J. Log. Algebr. Methods Program."},{"key":"10.1016\/j.tcs.2025.115705_bib0056","series-title":"Implementation and Application of Automata","first-page":"169","article-title":"LALBLC a program testing the equivalence of dpda\u2019s","author":"Henry","year":"2013"},{"issue":"3","key":"10.1016\/j.tcs.2025.115705_bib0057","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.2025.115705_bib0058","series-title":"MFCS\u201995, Proceedings","first-page":"423","article-title":"An elementary bisimulation decision procedure for arbitrary context-free processes","volume":"969","author":"Burkart","year":"1995"},{"issue":"1&2","key":"10.1016\/j.tcs.2025.115705_bib0059","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."}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397525006425?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397525006425?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T18:40:28Z","timestamp":1773081628000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397525006425"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,4]]},"references-count":59,"alternative-id":["S0304397525006425"],"URL":"https:\/\/doi.org\/10.1016\/j.tcs.2025.115705","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2026,4]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Subtyping 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.2025.115705","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2025 The Author(s). Published by Elsevier B.V.","name":"copyright","label":"Copyright"}],"article-number":"115705"}}