{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:34:49Z","timestamp":1750221289323,"version":"3.41.0"},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2017,12,27]],"date-time":"2017-12-27T00:00:00Z","timestamp":1514332800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000608","name":"London Mathematical Society","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000608","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-14-CE25-0007"],"award-info":[{"award-number":["ANR-14-CE25-0007"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,1]]},"abstract":"<jats:p>Higher-order recursion schemes (HORS) have recently emerged as a promising foundation for higher-order program verification. We examine the impact of enriching HORS with linear types. To that end, we introduce two frameworks that blend non-linear and linear types: a variant of the \u03bbY -calculus and an extension of HORS, called linear HORS (LHORS).<\/jats:p>\n          <jats:p>First we prove that the two formalisms are equivalent and there exist polynomial-time translations between them. Then, in order to support model-checking of (trees generated by) LHORS, we propose a refined version of alternating parity tree automata, called LNAPTA, whose behaviour depends on information about linearity. We show that the complexity of LNAPTA model-checking for LHORS depends on two type-theoretic parameters: linear order and linear depth. The former is in general smaller than the standard notion of order and ignores linear function spaces. In contrast, the latter measures the depth of linear clusters inside a type. Our main result states that LNAPTA model-checking of LHORS of linear order n is n-EXPTIME-complete, when linear depth is fixed. This generalizes and improves upon the classic result of Ong, which relies on the standard notion of order.<\/jats:p>\n          <jats:p>To illustrate the significance of the result, we consider two applications: the MSO model-checking problem on variants of HORS with case distinction (RSFD and HORSC) on a finite domain and a call-by-value resource verification problem. In both cases, decidability can be established by translation into HORS, but the implied complexity bounds will be suboptimal due to increases in type order. In contrast, we show that the complexity bounds derived by translations into LHORS and appealing to our result are optimal in that they match the respective hardness results.<\/jats:p>","DOI":"10.1145\/3158127","type":"journal-article","created":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T14:21:49Z","timestamp":1514557309000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Linearity in higher-order recursion schemes"],"prefix":"10.1145","volume":"2","author":[{"given":"Pierre","family":"Clairambault","sequence":"first","affiliation":[{"name":"University of Lyon, France \/ CNRS, France \/ ENS Lyon, France \/ Claude Bernard University Lyon 1, France \/ LIP, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Charles","family":"Grellois","sequence":"additional","affiliation":[{"name":"Inria, France \/ Aix-Marseille University, France \/ CNRS, France \/ ENSAM, France \/ University of Toulon, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrzej S.","family":"Murawski","sequence":"additional","affiliation":[{"name":"University of Oxford, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,12,27]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-3(3:1)2007"},{"key":"e_1_2_2_2_1","volume-title":"Technical Report LFCS-96-347. LFCS, Division of Informatics","author":"Barber A.","year":"1996","unstructured":"A. Barber and G. Plotkin . 1996 . Dual Intuitionistic Linear Logic . Technical Report LFCS-96-347. LFCS, Division of Informatics , University of Edinburgh. A. Barber and G. Plotkin. 1996. Dual Intuitionistic Linear Logic. Technical Report LFCS-96-347. LFCS, Division of Informatics, University of Edinburgh."},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1020891112409"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500589"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.40"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.73"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-08138-0_5"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48057-1_20"},{"key":"e_1_2_2_11_1","volume-title":"Proceedings of CSL. 260\u2013276","author":"Grellois C.","year":"2015","unstructured":"C. Grellois and P.-A. Melli\u00e8s . 2015 b. Relational Semantics of Linear Logic and Higher-order Model Checking . In Proceedings of CSL. 260\u2013276 . C. Grellois and P.-A. Melli\u00e8s. 2015b. Relational Semantics of Linear Logic and Higher-order Model Checking. In Proceedings of CSL. 260\u2013276."},{"key":"e_1_2_2_12_1","unstructured":"A. Haddad. 2013. Shape-Preserving Transformations of Higher-Order Recursion Schemes. Th\u00e8se de Doctorat. Universit\u00e9 Paris Diderot - Paris 7.  A. Haddad. 2013. Shape-Preserving Transformations of Higher-Order Recursion Schemes. Th\u00e8se de Doctorat. Universit\u00e9 Paris Diderot - Paris 7."},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.34"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005120"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46541-3_24"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480933"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.29"},{"key":"e_1_2_2_18_1","volume-title":"Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus. Logical Methods in Computer Science 7, 4","author":"Kobayashi N.","year":"2011","unstructured":"N. Kobayashi and C.-H. L. Ong . 2011. Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus. Logical Methods in Computer Science 7, 4 ( 2011 ). N. Kobayashi and C.-H. L. Ong. 2011. Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus. Logical Methods in Computer Science 7, 4 (2011)."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993525"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706355"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.10.022"},{"key":"e_1_2_2_22_1","unstructured":"P.-A. Melli\u00e8s. 2014. Linear logic and higher-order model-checking. Talk at Institut Henri Poincar\u00e9 http:\/\/www.pps. univ- paris- diderot.fr\/~mellies\/slides\/workshop- IHP- model- checking.pdf .  P.-A. Melli\u00e8s. 2014. Linear logic and higher-order model-checking. Talk at Institut Henri Poincar\u00e9 http:\/\/www.pps. univ- paris- diderot.fr\/~mellies\/slides\/workshop- IHP- model- checking.pdf ."},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837667"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364578"},{"key":"e_1_2_2_25_1","unstructured":"M. Nivat. 1972. On the interpretation of recursive program schemes. In Symposia Matematica.  M. Nivat. 1972. On the interpretation of recursive program schemes. In Symposia Matematica."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.38"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093883461"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535873"},{"key":"e_1_2_2_29_1","first-page":"229","article-title":"A Model for Behavioural Properties of Higher-order Programs","volume":"41","author":"Salvati S.","year":"2015","unstructured":"S. Salvati and I. Walukiewicz . 2015 . A Model for Behavioural Properties of Higher-order Programs . In Proceedings of CSL (LIPIcs) , Vol. 41. 229 \u2013 243 . S. Salvati and I. Walukiewicz. 2015. A Model for Behavioural Properties of Higher-order Programs. In Proceedings of CSL (LIPIcs), Vol. 41. 229\u2013243.","journal-title":"Proceedings of CSL (LIPIcs)"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000590"},{"key":"e_1_2_2_31_1","unstructured":"O. Serre. 2013. Playing with Trees and Logic. Habilitation \u00e0 Diriger des Recherches. Universit\u00e9 Paris Diderot - Paris 7. http:\/\/www.liafa.univ- paris- diderot.fr\/~serre\/papers\/HDR.pdf  O. Serre. 2013. Playing with Trees and Logic. Habilitation \u00e0 Diriger des Recherches. Universit\u00e9 Paris Diderot - Paris 7. http:\/\/www.liafa.univ- paris- diderot.fr\/~serre\/papers\/HDR.pdf"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(04)00081-8"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12032-9_24"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54830-7_12"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158127","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158127","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:30Z","timestamp":1750212690000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158127"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,27]]},"references-count":33,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1145\/3158127"],"URL":"https:\/\/doi.org\/10.1145\/3158127","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2017,12,27]]},"assertion":[{"value":"2017-12-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}