{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T22:31:40Z","timestamp":1673476300679},"reference-count":37,"publisher":"Cambridge University Press (CUP)","issue":"7","license":[{"start":{"date-parts":[[2015,3,18]],"date-time":"2015-03-18T00:00:00Z","timestamp":1426636800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2016,10]]},"abstract":"<jats:p>Simply typed \u03bb-calculus with fixpoint combinators, \u03bb<jats:italic>Y<\/jats:italic>-calculus, offers an interesting method for approximating program semantics. The B\u00f6hm tree of a \u03bb<jats:italic>Y<\/jats:italic>-term represents the meaning of the program up to the meaning of built-in constants. It is much easier to reason about properties of such trees than properties of interpreted programs. Moreover, some interesting properties of programs are already expressible on the level of these trees.<\/jats:p><jats:p>Collapsible pushdown automata (CPDA) give another way of generating the same class of trees as \u03bb<jats:italic>Y<\/jats:italic>-terms. We clarify the relationship between the two models. In particular, we present two relatively simple translations from \u03bb<jats:italic>Y<\/jats:italic>-terms to CPDA using Krivine machines as an intermediate step. The latter are general machines for describing computation of the weak head normal form in the \u03bb-calculus. They provide the notions of closure and environment that facilitate reasoning about computation.<\/jats:p>","DOI":"10.1017\/s0960129514000590","type":"journal-article","created":{"date-parts":[[2015,3,18]],"date-time":"2015-03-18T18:19:31Z","timestamp":1426702771000},"page":"1304-1350","source":"Crossref","is-referenced-by-count":5,"title":["Simply typed fixpoint calculus and collapsible pushdown automata"],"prefix":"10.1017","volume":"26","author":[{"given":"SYLVAIN","family":"SALVATI","sequence":"first","affiliation":[]},{"given":"IGOR","family":"WALUKIEWICZ","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2015,3,18]]},"reference":[{"key":"S0960129514000590_ref2","doi-asserted-by":"publisher","DOI":"10.1145\/321479.321488"},{"key":"S0960129514000590_ref31","first-page":"255","article-title":"On the interpretation of recursive program schemes. In:","volume":"15","author":"Nivat","year":"1972","journal-title":"Symposia Mathematica"},{"key":"S0960129514000590_ref23","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487246"},{"key":"S0960129514000590_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71129-7"},{"key":"S0960129514000590_ref28","doi-asserted-by":"crossref","unstructured":"Milner R. (1973) Models of LCF. Memo AIM-186, Stanford University.","DOI":"10.21236\/AD0758645"},{"key":"S0960129514000590_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45931-6_15"},{"key":"S0960129514000590_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-007-9018-9"},{"key":"S0960129514000590_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/11417170_5"},{"key":"S0960129514000590_ref19","unstructured":"Kfoury A. and Urzyczyn P. (1988) Finitely typed functional programs, Part II: Comparisons to imperative languages. Technical report BUCS tech report, 88-012, Boston University."},{"key":"S0960129514000590_ref30","unstructured":"Nivat M. (1972a) Langages alg\u00e9briques sur le magma libre et s\u00e9mantique des sch\u00e9mas de programme. In: Proceedings of the International Colloquium on Automata, Languages and Programming 293\u2013308."},{"key":"S0960129514000590_ref14","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(86)80016-X"},{"key":"S0960129514000590_ref37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38946-7_15"},{"key":"S0960129514000590_ref33","doi-asserted-by":"crossref","unstructured":"Parys P. (2012) On the significance of the collapse operation. In: Proceedings of the Annual Symposium on Logic in Computer Science, IEEE Computer Society 521\u2013530.","DOI":"10.1109\/LICS.2012.62"},{"key":"S0960129514000590_ref5","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2008.09.003"},{"key":"S0960129514000590_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22012-8_12"},{"key":"S0960129514000590_ref29","unstructured":"Miranda J. G. de (2006) Structures Generated by Higher-Order Grammars and the Safety Constraint, Ph.D. thesis, Oxford University."},{"key":"S0960129514000590_ref4","volume-title":"The Lambda Calculus, Its Syntax and Semantics","author":"Barendregt","year":"1985"},{"key":"S0960129514000590_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31585-5_18"},{"key":"S0960129514000590_ref15","doi-asserted-by":"publisher","DOI":"10.2969\/msjmemoirs\/00201C020"},{"key":"S0960129514000590_ref13","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90009-3"},{"key":"S0960129514000590_ref7","doi-asserted-by":"crossref","unstructured":"Broadbent C. , Carayol A. , Ong L. and Serre O. (2010) Recursion schemes and logical reflection. In: Proceedings of the Annual Symposium on Logic in Computer Science, IEEE Computer Society 120\u2013129.","DOI":"10.1109\/LICS.2010.40"},{"key":"S0960129514000590_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45687-2_13"},{"key":"S0960129514000590_ref24","doi-asserted-by":"crossref","unstructured":"Kobayashi N. and Ong L. (2009) A type system equivalent to modal mu-calculus model checking of recursion schemes. In: Proceedings of the Annual Symposium on Logic in Computer Science, IEEE Computer Society 179\u2013188.","DOI":"10.1109\/LICS.2009.29"},{"key":"S0960129514000590_ref10","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.73"},{"key":"S0960129514000590_ref17","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2917"},{"key":"S0960129514000590_ref34","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"S0960129514000590_ref36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33512-9_2"},{"key":"S0960129514000590_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24597-1_10"},{"key":"S0960129514000590_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/11523468_117"},{"key":"S0960129514000590_ref26","first-page":"1170","article-title":"The hierarchy of indexed languages of an arbitrary level.","volume":"15","author":"Maslov","year":"1974","journal-title":"Soviet Mathematics Doklady"},{"key":"S0960129514000590_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19805-2_18"},{"key":"S0960129514000590_ref27","first-page":"38","article-title":"Multilevel stack automata.","volume":"12","author":"Maslov","year":"1976","journal-title":"Problems of Information Transmission"},{"key":"S0960129514000590_ref9","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.41"},{"key":"S0960129514000590_ref16","doi-asserted-by":"crossref","unstructured":"Hague M. , Murawski A. S. , Ong C.-H. L. and Serre O. (2008) Collapsible pushdown automata and recursion schemes. In: Proceedings of the Annual Symposium on Logic in Computer Science, IEEE Computer Society 452\u2013461.","DOI":"10.1109\/LICS.2008.34"},{"key":"S0960129514000590_ref32","doi-asserted-by":"crossref","unstructured":"Ong C.-H. L. (2006) On model-checking trees generated by higher-order recursion schemes. In: Proceedings of the Annual Symposium on Logic in Computer Science, IEEE Computer Society 81\u201390.","DOI":"10.1109\/LICS.2006.38"},{"key":"S0960129514000590_ref18","first-page":"82","volume-title":"Problems of Cybernetics I","author":"Ianov","year":"1969"},{"key":"S0960129514000590_ref6","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-5(1:3)2009"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129514000590","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,22]],"date-time":"2019-08-22T03:41:08Z","timestamp":1566445268000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129514000590\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,3,18]]},"references-count":37,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2016,10]]}},"alternative-id":["S0960129514000590"],"URL":"https:\/\/doi.org\/10.1017\/s0960129514000590","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,3,18]]}}}