{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:22:06Z","timestamp":1751660526636,"version":"3.41.0"},"reference-count":56,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2016,12,15]],"date-time":"2016-12-15T00:00:00Z","timestamp":1481760000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM SIGLOG News"],"published-print":{"date-parts":[[2016,12,15]]},"abstract":"<jats:p>In verification, an automata theoretic approach is by now a standard. In order to extend this approach to higher-order programs we need a good understanding of higher-order control flow, and for this semantics has the right tools. We present some results and methods of this subject between automata theory and semantics.<\/jats:p>","DOI":"10.1145\/3026744.3026745","type":"journal-article","created":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T18:30:41Z","timestamp":1585938641000},"page":"13-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Automata theory and higher-order model-checking"],"prefix":"10.1145","volume":"3","author":[{"given":"Igor","family":"Walukiewicz","sequence":"first","affiliation":[{"name":"Bordeaux University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2016,12,15]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-3(3:1)2007"},{"key":"e_1_2_1_2_1","volume-title":"Amadio and Pierre-Louis Curien","author":"Roberto","year":"1998","unstructured":"Roberto M. Amadio and Pierre-Louis Curien . 1998 . Domains and Lambda-Calculi. Cambridge Tracts in Theoretical Computer Science, Vol. 46 . Cambridge University Press . Roberto M. Amadio and Pierre-Louis Curien. 1998. Domains and Lambda-Calculi. Cambridge Tracts in Theoretical Computer Science, Vol. 46. Cambridge University Press."},{"key":"e_1_2_1_3_1","volume-title":"Model-Checking of Ordered Multi-Pushdown Automata. Log. Methods Comput. Sci. 8, 3 (09","author":"Atig Mohamed F.","year":"2012","unstructured":"Mohamed F. Atig . 2012. Model-Checking of Ordered Multi-Pushdown Automata. Log. Methods Comput. Sci. 8, 3 (09 2012 ). Mohamed F. Atig. 2012. Model-Checking of Ordered Multi-Pushdown Automata. Log. Methods Comput. Sci. 8, 3 (09 2012)."},{"key":"e_1_2_1_5_1","volume-title":"The Safe Lambda Calculus. Logical Methods in Computer Science 5, 1","author":"Blum William","year":"2009","unstructured":"William Blum and C.-H. Luke Ong . 2009. The Safe Lambda Calculus. Logical Methods in Computer Science 5, 1 ( 2009 ). William Blum and C.-H. Luke Ong. 2009. The Safe Lambda Calculus. Logical Methods in Computer Science 5, 1 (2009)."},{"volume-title":"Logic and Automata (Texts in Logic and Games), J\u00f6rg Flum, Erich Gr\u00e4del","author":"Blumensath Achim","key":"e_1_2_1_6_1","unstructured":"Achim Blumensath , Thomas Colcombet , and Christof L\u00f6ding . 2008. Logical theories and compatible operations . In Logic and Automata (Texts in Logic and Games), J\u00f6rg Flum, Erich Gr\u00e4del , and Thomas Wilke (Eds.), Vol. 2 . Amsterdam University Press , 73--106. Achim Blumensath, Thomas Colcombet, and Christof L\u00f6ding. 2008. Logical theories and compatible operations. In Logic and Automata (Texts in Logic and Games), J\u00f6rg Flum, Erich Gr\u00e4del, and Thomas Wilke (Eds.), Vol. 2. Amsterdam University Press, 73--106."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500589"},{"key":"e_1_2_1_8_1","volume-title":"Broadbent and Naoki Kobayashi","author":"Christopher","year":"2013","unstructured":"Christopher H. Broadbent and Naoki Kobayashi . 2013 . Saturation-Based Model Checking of Higher-Order Recursion Schemes. In CSL (LIPIcs), Vol. 23 . Schloss Dagstuhl , 129--148. Christopher H. Broadbent and Naoki Kobayashi. 2013. Saturation-Based Model Checking of Higher-Order Recursion Schemes. In CSL (LIPIcs), Vol. 23. Schloss Dagstuhl, 129--148."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19600060105"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.73"},{"key":"e_1_2_1_11_1","volume-title":"Ordered Tree-Pushdown Systems. In FSTTCS'15 (LIPIcs)","volume":"45","author":"Clemente Lorenzo","year":"2015","unstructured":"Lorenzo Clemente , Pawel Parys , Sylvain Salvati , and Igor Walukiewicz . 2015 . Ordered Tree-Pushdown Systems. In FSTTCS'15 (LIPIcs) , Vol. 45 . 163--177. Lorenzo Clemente, Pawel Parys, Sylvain Salvati, and Igor Walukiewicz. 2015. Ordered Tree-Pushdown Systems. In FSTTCS'15 (LIPIcs), Vol. 45. 163--177."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(78)90008-7"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90268-2"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00049-3"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00012-9"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(97)00048-1"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90009-3"},{"key":"e_1_2_1_18_1","unstructured":"S. Eilenberg. 1974. Automata Languages and Machines. Vol. A. Academic Press New York.   S. Eilenberg. 1974. Automata Languages and Machines. Vol. A. Academic Press New York."},{"key":"e_1_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Calvin C. Elgot. 1971. Algebraic theories and program schemes. See Engeler {1991} 71--88.  Calvin C. Elgot. 1971. Algebraic theories and program schemes. See Engeler {1991} 71--88.","DOI":"10.1007\/BFb0059694"},{"key":"e_1_2_1_20_1","volume-title":"Symposium on Semantics of Algorithmic Languages. Lecture Notes in Mathematics","volume":"188","author":"Ed Erwin Engeler","year":"1991","unstructured":"Erwin Engeler ( Ed .). 1991 . Symposium on Semantics of Algorithmic Languages. Lecture Notes in Mathematics , Vol. 188 . Springer. Erwin Engeler (Ed.). 1991. Symposium on Semantics of Algorithmic Languages. Lecture Notes in Mathematics, Vol. 188. Springer."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/800061.808767"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(77)80034-2"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90051-X"},{"key":"e_1_2_1_25_1","volume-title":"Finitary Semantics of Linear Logic and Higher-Order Model-Checking. In MFCS'15 (LNCS)","volume":"9234","author":"Grellois Charles","year":"2015","unstructured":"Charles Grellois and Paul-Andr\u00e9 Melli\u00e8s . 2015 . Finitary Semantics of Linear Logic and Higher-Order Model-Checking. In MFCS'15 (LNCS) , Vol. 9234 . 256--268. Charles Grellois and Paul-Andr\u00e9 Melli\u00e8s. 2015. Finitary Semantics of Linear Logic and Higher-Order Model-Checking. In MFCS'15 (LNCS), Vol. 9234. 256--268."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.34"},{"volume-title":"The logical schemes of algorithms","author":"Ianov Y.","key":"e_1_2_1_27_1","unstructured":"Y. Ianov . 1960. The logical schemes of algorithms . In Problems of Cybernetics I. Pergamon , Oxford , 82--140. Y. Ianov. 1960. The logical schemes of algorithms. In Problems of Cybernetics I. Pergamon, Oxford, 82--140."},{"key":"e_1_2_1_28_1","volume-title":"Schemes with Recursion on Higher Types. In MFCS'76 (LNCS)","volume":"45","author":"Indermark Klaus","year":"1976","unstructured":"Klaus Indermark . 1976 . Schemes with Recursion on Higher Types. In MFCS'76 (LNCS) , Vol. 45 . 352--358. Klaus Indermark. 1976. Schemes with Recursion on Higher Types. In MFCS'76 (LNCS), Vol. 45. 352--358."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.51"},{"key":"e_1_2_1_30_1","doi-asserted-by":"crossref","unstructured":"T. Knapik D. Niwinski and P. Urzyczyn. 2002. Higher-order pushdown trees are easy. In FoSSaCS' 02 (LNCS) Vol. 2303. 205--222.   T. Knapik D. Niwinski and P. Urzyczyn. 2002. Higher-order pushdown trees are easy. In FoSSaCS' 02 (LNCS) Vol. 2303. 205--222.","DOI":"10.1007\/3-540-45931-6_15"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487246"},{"key":"e_1_2_1_32_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 Naoki","year":"2011","unstructured":"Naoki Kobayashi and C.-H. Luke Ong . 2011. Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus. Logical Methods in Computer Science 7, 4 ( 2011 ). Naoki Kobayashi and C.-H. Luke 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_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.29"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-007-9018-9"},{"volume-title":"Logic, Meaning and Computation: Essays in memory of Alonzo Church","author":"Loader R.","key":"e_1_2_1_35_1","unstructured":"R. Loader . 2001. The Undecidability of lambda-definability . In Logic, Meaning and Computation: Essays in memory of Alonzo Church , C. A. Anderson and M. Zeleny (Eds.). Kluwer , 331--342. R. Loader. 2001. The Undecidability of lambda-definability. In Logic, Meaning and Computation: Essays in memory of Alonzo Church, C. A. Anderson and M. Zeleny (Eds.). Kluwer, 331--342."},{"volume-title":"Models of LCF. Memo AIM-186","author":"Milner Robin","key":"e_1_2_1_36_1","unstructured":"Robin Milner . 1973. Models of LCF. Memo AIM-186 . Stanford University . Robin Milner. 1973. Models of LCF. Memo AIM-186. Stanford University."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90087-8"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837667"},{"key":"e_1_2_1_39_1","first-page":"255","article-title":"On interpretation of polyadic recursive program schemes","volume":"15","author":"Nivat M.","year":"1975","unstructured":"M. Nivat . 1975 . On interpretation of polyadic recursive program schemes . Symposia Mathematica 15 (1975), 255 -- 281 . M. Nivat. 1975. On interpretation of polyadic recursive program schemes. Symposia Mathematica 15 (1975), 255--281.","journal-title":"Symposia Mathematica"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.38"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.9"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535873"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02261-6_5"},{"key":"e_1_2_1_45_1","volume-title":"FSTCS (LIPIcs)","volume":"24","author":"Salvati Sylvain","year":"2013","unstructured":"Sylvain Salvati and Igor Walukiewicz . 2013 . Evaluation is MSOL-compatible . In FSTCS (LIPIcs) , Vol. 24 . Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 103--114. Sylvain Salvati and Igor Walukiewicz. 2013. Evaluation is MSOL-compatible. In FSTCS (LIPIcs), Vol. 24. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 103--114."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.07.012"},{"key":"e_1_2_1_47_1","volume-title":"CSL'15 (LIPIcs)","volume":"41","author":"Salvati Sylvain","year":"2015","unstructured":"Sylvain Salvati and Igor Walukiewicz . 2015 a. A Model for Behavioural Properties of Higher-order Programs . In CSL'15 (LIPIcs) , Vol. 41 . 229--243. Sylvain Salvati and Igor Walukiewicz. 2015a. A Model for Behavioural Properties of Higher-order Programs. In CSL'15 (LIPIcs), Vol. 41. 229--243."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46678-0_22"},{"key":"e_1_2_1_49_1","volume-title":"Using models to model-check recursive schemes. Logical Methods in Computer Science 11, 2","author":"Salvati Sylvain","year":"2015","unstructured":"Sylvain Salvati and Igor Walukiewicz . 2015c. Using models to model-check recursive schemes. Logical Methods in Computer Science 11, 2 ( 2015 ). Sylvain Salvati and Igor Walukiewicz. 2015c. Using models to model-check recursive schemes. Logical Methods in Computer Science 11, 2 (2015)."},{"key":"e_1_2_1_50_1","volume-title":"Simply typed fixpoint calculus and collapsible push-down automata. Mathematical Structures in Computer Science FirstView (4","author":"Salvati Sylvain","year":"2016","unstructured":"Sylvain Salvati and Igor Walukiewicz . 2016. Simply typed fixpoint calculus and collapsible push-down automata. Mathematical Structures in Computer Science FirstView (4 2016 ), 1--47. Sylvain Salvati and Igor Walukiewicz. 2016. Simply typed fixpoint calculus and collapsible push-down automata. Mathematical Structures in Computer Science FirstView (4 2016), 1--47."},{"key":"e_1_2_1_51_1","volume-title":"Continuous Lattices. In Proc. of Dalhousie Conference (Lecture Notes in Mathematics)","volume":"188","author":"Scott D.","year":"1972","unstructured":"D. Scott . 1972 . Continuous Lattices. In Proc. of Dalhousie Conference (Lecture Notes in Mathematics) , Vol. 188 . Springer, 311--366. D. Scott. 1972. Continuous Lattices. In Proc. of Dalhousie Conference (Lecture Notes in Mathematics), Vol. 188. Springer, 311--366."},{"key":"e_1_2_1_52_1","doi-asserted-by":"crossref","unstructured":"Dana S. Scott. 1971. The lattice of flow diagrams. See Engeler {1991} 311--366.  Dana S. Scott. 1971. The lattice of flow diagrams. See Engeler {1991} 311--366.","DOI":"10.1007\/BFb0059703"},{"volume-title":"MFCS'84 (LNCS)","author":"Semenov A. L.","key":"e_1_2_1_53_1","unstructured":"A. L. Semenov . 1984. Decidability of Monadic Theories . In MFCS'84 (LNCS) , Vol. 176 . Springer-Verlag , 162--175. A. L. Semenov. 1984. Decidability of Monadic Theories. In MFCS'84 (LNCS), Vol. 176. Springer-Verlag, 162--175."},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00285-1"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00027-0"},{"key":"e_1_2_1_56_1","volume-title":"Deciding DPDA Equivalence Is Primitive Recursive. In ICALP'02 (LNCS)","volume":"2380","author":"Stirling Colin","year":"2002","unstructured":"Colin Stirling . 2002 . Deciding DPDA Equivalence Is Primitive Recursive. In ICALP'02 (LNCS) , Vol. 2380 . 821--832. Colin Stirling. 2002. Deciding DPDA Equivalence Is Primitive Recursive. In ICALP'02 (LNCS), Vol. 2380. 821--832."},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603133"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00185-2"}],"container-title":["ACM SIGLOG News"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3026744.3026745","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3026744.3026745","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:03:29Z","timestamp":1750215809000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3026744.3026745"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,12,15]]},"references-count":56,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2016,12,15]]}},"alternative-id":["10.1145\/3026744.3026745"],"URL":"https:\/\/doi.org\/10.1145\/3026744.3026745","relation":{},"ISSN":["2372-3491"],"issn-type":[{"type":"electronic","value":"2372-3491"}],"subject":[],"published":{"date-parts":[[2016,12,15]]},"assertion":[{"value":"2016-12-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}