{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:34:23Z","timestamp":1750307663261,"version":"3.41.0"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2009,8,1]],"date-time":"2009-08-01T00:00:00Z","timestamp":1249084800000},"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 Trans. Comput. Logic"],"published-print":{"date-parts":[[2009,8]]},"abstract":"<jats:p>\n            We extend Meyer and Ritchie's Loop language with higher-order procedures and procedural variables and we show that the resulting programming language (called Loop\n            <jats:sup>\u03c9<\/jats:sup>\n            ) is a natural imperative counterpart of G\u00f6del System T. The argument is two-fold:\n          <\/jats:p>\n          <jats:p>\n            (1) we define a translation of the Loop\n            <jats:sup>\u03c9<\/jats:sup>\n            language into System T and we prove that this translation actually provides a lock-step simulation,\n          <\/jats:p>\n          <jats:p>\n            (2) using a converse translation, we show that Loop\n            <jats:sup>\u03c9<\/jats:sup>\n            is expressive enough to encode any term of System T.\n          <\/jats:p>\n          <jats:p>\n            Moreover, we define the \u201citeration rank\u201d of a Loop\n            <jats:sup>\u03c9<\/jats:sup>\n            program, which corresponds to the classical notion of \u201crecursion rank\u201d in System T, and we show that both translations preserve ranks. Two applications of these results in the area of implicit complexity are described.\n          <\/jats:p>","DOI":"10.1145\/1555746.1555750","type":"journal-article","created":{"date-parts":[[2009,8,11]],"date-time":"2009-08-11T13:29:23Z","timestamp":1249997363000},"page":"1-37","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Extending the loop language with higher-order procedural variables"],"prefix":"10.1145","volume":"10","author":[{"given":"Tristan","family":"Crolard","sequence":"first","affiliation":[{"name":"Paris East University, Cr\u00e9teil Cedex, France"}]},{"given":"Emmanuel","family":"Polonowski","sequence":"additional","affiliation":[{"name":"Paris East University, Cr\u00e9teil Cedex, France"}]},{"given":"Pierre","family":"Valarcher","sequence":"additional","affiliation":[{"name":"Paris East University, Cr\u00e9teil Cedex, France"}]}],"member":"320","published-online":{"date-parts":[[2009,8,14]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"crossref","unstructured":"Appel A. W. 1998. Modern Compiler Implementation in ML. Cambridge University Press Cambridge UK.   Appel A. W. 1998. Modern Compiler Implementation in ML. Cambridge University Press Cambridge UK.","DOI":"10.1017\/CBO9780511811449"},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Avigad J. and Feferman S. 1998. G&amp;#246;del's functional (&amp;#8220;dialectica&amp;#8221;) interpretation. In Handbook of Proof Theory S. R. Buss Ed. Elsevier Science Publishers 337--405.  Avigad J. and Feferman S. 1998. G&amp;#246;del's functional (&amp;#8220;dialectica&amp;#8221;) interpretation. In Handbook of Proof Theory S. R. Buss Ed. Elsevier Science Publishers 337--405.","DOI":"10.1016\/S0049-237X(98)80020-7"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001530050160"},{"key":"e_1_2_1_4_1","unstructured":"Calude C. 1988. Theories of Computational Complexity. Elsevier Science Inc.   Calude C. 1988. Theories of Computational Complexity. Elsevier Science Inc."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90039-5"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00011-5"},{"key":"e_1_2_1_7_1","first-page":"1","article-title":"On the expressive power of the loop language","volume":"13","author":"Crolard T.","year":"2006","journal-title":"Nordic J. Comput."},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Davis M. and Weyuker E. 1983. Computability Complexity and Languages. Academic Press.   Davis M. and Weyuker E. 1983. Computability Complexity and Languages. Academic Press.","DOI":"10.1016\/B978-0-12-206380-0.50020-1"},{"key":"e_1_2_1_9_1","unstructured":"DOD. 1980. The Programming Language Ada. Reference Manual. Springer.  DOD. 1980. The Programming Language Ada. Reference Manual. Springer."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00264468"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/41625.41654"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.178047"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680200446X"},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of the Formal Methods and Software Engineering, 6th International Conference on Formal Engineering Methods, (ICFEM'04)","volume":"3308","author":"Filli","year":"2004"},{"volume-title":"Proceedings of the 6th Ade-Europe International Conference","author":"Gellerich W.","key":"e_1_2_1_15_1"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/319838.319848"},{"key":"e_1_2_1_17_1","unstructured":"Girard J.-Y. Lafont Y. and Taylor P. 1989. Proofs and Types. Vol. 7. Cambridge Tracts in Theoretical Computer Science.   Girard J.-Y. Lafont Y. and Taylor P. 1989. Proofs and Types. Vol. 7. Cambridge Tracts in Theoretical Computer Science."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1746-8361.1958.tb01464.x"},{"key":"e_1_2_1_19_1","unstructured":"G&amp;#246;del K. 1990. Collected Works vol. 2. Oxford University Press Oxford UK.  G&amp;#246;del K. 1990. Collected Works vol. 2. Oxford University Press Oxford UK."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002748"},{"key":"e_1_2_1_21_1","unstructured":"ISO. 2003. C&amp;num; language specification ISO\/IEC 23270.   ISO. 2003. C&amp;num; language specification ISO\/IEC 23270."},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Jones N. D. 1997. Computability and Complexity from a Programming Perspective. The MIT Press.   Jones N. D. 1997. Computability and Complexity from a Programming Perspective. The MIT Press.","DOI":"10.7551\/mitpress\/2003.001.0001"},{"volume-title":"Proceedings of the Symposium on Theoretical Aspects of Computer Science (STACS)","series-title":"Lecture Notes in Computer Science","author":"Kahn G.","key":"e_1_2_1_23_1"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010051815785"},{"key":"e_1_2_1_25_1","first-page":"241","article-title":"On the interpretation of non-finitist proofs&amp;#8212;part I","volume":"16","author":"Kreisel G.","year":"1951","journal-title":"J. Symb. Log"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/6.4.308"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/367177.367199"},{"volume-title":"Proceedings of the ACM Natural Meeting.","author":"Meyer A. R.","key":"e_1_2_1_28_1"},{"key":"e_1_2_1_29_1","doi-asserted-by":"crossref","unstructured":"Milner R. Tofte M. Harper R. and MacQueen D. 1997. The Definition of Standard ML. Rev. Ed. MIT Press.   Milner R. Tofte M. Harper R. and MacQueen D. 1997. The Definition of Standard ML. Rev. Ed. MIT Press.","DOI":"10.7551\/mitpress\/2319.001.0001"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_2_1_31_1","doi-asserted-by":"crossref","unstructured":"O'Hearn P. W. and Tennent R. D. Eds. 1997. Algol-Like Languages. Birkha&amp;#252;ser.   O'Hearn P. W. and Tennent R. D. Eds. 1997. Algol-Like Languages. Birkha&amp;#252;ser.","DOI":"10.1007\/978-1-4612-4118-8"},{"key":"e_1_2_1_32_1","unstructured":"Peter R. 1968. Recursive Functions. Academic Press.  Peter R. 1968. Recursive Functions. Academic Press."},{"key":"e_1_2_1_33_1","unstructured":"Plotkin G. 1981. A structural approach to operational semantics. Tech. rep. DAIMI FN-19 Aarhus University.  Plotkin G. 1981. A structural approach to operational semantics. Tech. rep. DAIMI FN-19 Aarhus University."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512766"},{"key":"e_1_2_1_35_1","unstructured":"Reynolds J. C. 1981. The essence of Algol. In Algorithmic Languages de Bakker and van Vliet Eds. IFIP North-Holland Amsterdam 345--372.  Reynolds J. C. 1981. The essence of Algol. In Algorithmic Languages de Bakker and van Vliet Eds. IFIP North-Holland Amsterdam 345--372."},{"key":"e_1_2_1_36_1","doi-asserted-by":"crossref","unstructured":"Reynolds J. C. 1998. Theories of Programming Languages. Cambridge University Press.   Reynolds J. C. 1998. Theories of Programming Languages. Cambridge University Press.","DOI":"10.1017\/CBO9780511626364"},{"key":"e_1_2_1_37_1","unstructured":"Schmidt D. A. 1994. The Structure of Typed Programming Languages. The MIT Press.   Schmidt D. A. 1994. The Structure of Typed Programming Languages. The MIT Press."},{"key":"e_1_2_1_38_1","unstructured":"Sch&amp;#252;tte K. 1967. Proof Theory. Addison Wesley.  Sch&amp;#252;tte K. 1967. Proof Theory. Addison Wesley."},{"key":"e_1_2_1_39_1","unstructured":"Stoy J. 1977. Denotational Semantics of Programming Languages: The Scott-Strachey Approach to Programming Language Theory. The MIT Press.   Stoy J. 1977. Denotational Semantics of Programming Languages: The Scott-Strachey Approach to Programming Language Theory. The MIT Press."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1046"},{"key":"e_1_2_1_41_1","first-page":"751","article-title":"Total functional programming","volume":"10","author":"Turner D. A.","year":"2004","journal-title":"J. Unin. Comput. Sci."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91592"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289429"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1555746.1555750","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1555746.1555750","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:29:31Z","timestamp":1750253371000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1555746.1555750"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,8]]},"references-count":43,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2009,8]]}},"alternative-id":["10.1145\/1555746.1555750"],"URL":"https:\/\/doi.org\/10.1145\/1555746.1555750","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2009,8]]},"assertion":[{"value":"2006-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2007-10-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-08-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}