{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,4]],"date-time":"2023-09-04T21:12:49Z","timestamp":1693861969060},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"5","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[1997,9]]},"abstract":"\n PIM is an equational logic designed to function as a \u201ctransformational toolkit\u201d for compilers and other programming tools that analyze and manipulate imperative languages. It has been applied to such problems as program slicing, symbolic evaluation, conditional constant propagation, and dependence analysis. PIM consists of the untyped lambda calculus extended with an algebraic data type that characterizes the behavior of lazy stores and generalized conditionals. A graph form of PIM terms is by design closely related to several intermediate representations commonly used in optimizing compilers. In this article, we show that PIM's core algebraic component, PIM\n \n t<\/jats:italic>\n <\/jats:sub>\n , possesses a\n complete<\/jats:italic>\n equational axiomatization (under the assumption of certain reasonable restrictions on term formation). This has the practical consequence of guaranteeing that every semantics-preserving transformation on a program representable in PIM\n \n t<\/jats:italic>\n <\/jats:sub>\n can be derived by application of PIM\n \n t<\/jats:italic>\n <\/jats:sub>\n rules. We systematically derive the complete PIM\n \n t<\/jats:italic>\n <\/jats:sub>\n logic as the culmination of a sequence of increasingly powerful equational systems starting from a straightforward \u201cinterpreter\u201d for closed PIM\n \n t<\/jats:italic>\n <\/jats:sub>\n terms. This work is an intermediate step in a larger program to develop a set of well-founded tools for manipulation of imperative programs by compilers and other systems that perform program analysis.\n <\/jats:p>","DOI":"10.1145\/265943.265944","type":"journal-article","created":{"date-parts":[[2002,10,7]],"date-time":"2002-10-07T13:52:47Z","timestamp":1033998767000},"page":"639-684","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Toward a complete transformational toolkit for compilers"],"prefix":"10.1145","volume":"19","author":[{"given":"J. A.","family":"Bergstra","sequence":"first","affiliation":[{"name":"Univ. of Amsterdam, Amsterdam, The Netherlands; and Utrecht Univ., Utrecht, The Netherlands"}]},{"given":"T. B.","family":"Dinesh","sequence":"additional","affiliation":[{"name":"CWI, Amsterdam, The Netherlands"}]},{"given":"J.","family":"Field","sequence":"additional","affiliation":[{"name":"IBM T. J. Watson Research Center, Yorktown Heights, NY"}]},{"given":"J.","family":"Heering","sequence":"additional","affiliation":[{"name":"CWI, Amsterdam, The Netherlands"}]}],"member":"320","published-online":{"date-parts":[[1997,9]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.126773"},{"key":"e_1_2_1_2_1","first-page":"257","volume-title":"Proceedings of the A CM SIGPLAN Conference on Programming Language Design and Implementation. ACM","author":"BALLANCE R. A.","year":"1990"},{"key":"e_1_2_1_3_1","first-page":"141","volume-title":"Proceedings of the PARLE Conference.","volume":"259","author":"BARENDREGT H.","year":"1987"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90057-4"},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0168-0072(94)00038-5","article-title":"The data type variety of stack algebras","volume":"73","author":"BERGSTRA J.","year":"1995","journal-title":"Ann. Pure Applied Logic"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.62091"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/4472.4474"},{"key":"e_1_2_1_8_1","volume-title":"Algebraic Methods in Semantics","author":"BOUDOL G."},{"key":"e_1_2_1_9_1","first-page":"13","volume-title":"Proceedings of the A CM SIGPLAN Conference on Programming Language Design and Implementation. ACM","author":"CARTWRIGHT R.","year":"1989"},{"key":"e_1_2_1_10_1","first-page":"146","volume-title":"Proceedings of the ACM SIG- PLAN Conference on Programming Language Design and Implementation. ACM","author":"CHAMBERS C.","year":"1989"},{"key":"e_1_2_1_11_1","first-page":"246","volume-title":"Proceedings of the ACM SIC- PLAN Conference on Programming Language Design and Implementation. ACM SIGPLAN Not. 30","author":"CLICK C.","year":"1995"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115320"},{"key":"e_1_2_1_13_1","first-page":"243","article-title":"Rewrite systems. In Handbook of Theoretical Computer Science. Vol. B, Formal Models and Semantics, J. van Leeuwen, Ed. Elsevier\/The MIT Press","author":"DERSHOWITZ N.","year":"1990","journal-title":"Amsterdam"},{"key":"e_1_2_1_14_1","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1016\/0304-3975(82)90111-6","article-title":"Mixed computation: Potential applications and problems for study","volume":"18","author":"ERSHOV A. P.","year":"1982","journal-title":"Theoret. Comput. Sci."},{"key":"e_1_2_1_15_1","first-page":"31","article-title":"Controlled mixed computation and its appplication to systematic development of language-oriented parsers. In Program Specification and Transformation, L. G. L. T. Meertens, Ed. North-Holland","author":"ERSHOV A. P.","year":"1987","journal-title":"Amsterdam"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(89)90069-8"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90014-7"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/24039.24041"},{"key":"e_1_2_1_19_1","first-page":"98","volume-title":"Proceedings of the A CM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation. ACM","author":"FIELD J.","year":"1992"},{"key":"e_1_2_1_20_1","first-page":"379","volume-title":"Proceedings of the 22nd A CM Symposium on Principles of Programming Languages. ACM","author":"FIELD J.","year":"1995"},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1016\/0304-3975(86)90173-8","article-title":"Partial evaluation and w-completeness of algebraic specifications","volume":"43","author":"HEERING J.","year":"1986","journal-title":"Theoret. Comput. Sci."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/27651.27653"},{"key":"e_1_2_1_26_1","first-page":"146","volume-title":"Proceedings of the 15th A CM Symposium on Principles of Programming Languages. ACM","author":"HORWITZ S.","year":"1988"},{"key":"e_1_2_1_27_1","first-page":"331","volume-title":"Ed. Lecture Notes in Computer Science","volume":"154","author":"HSIANG J.","year":"1983"},{"key":"e_1_2_1_28_1","unstructured":"JONES N. D. GOMARD C. K. AND SESTOFT P. 1993. Partial Evaluation and Automatic Program Generation. Prentice-Hall Englewood Cliffs N.J. JONES N. D. GOMARD C. K. AND SESTOFT P. 1993. Partial Evaluation and Automatic Program Generation. Prentice-Hall Englewood Cliffs N.J."},{"key":"e_1_2_1_29_1","first-page":"22","volume-title":"Lecture Notes in Computer Science","volume":"247","author":"KAHN G.","year":"1987"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177577"},{"key":"e_1_2_1_31_1","volume-title":"Handbook of Logic in Computer Science.","author":"KLOP J. W."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90033-E"},{"key":"e_1_2_1_33_1","first-page":"284","volume-title":"Proceedings of the gth IEEE Symposium on Logic in Computer Science. IEEE","author":"MASON I.","year":"1989"},{"key":"e_1_2_1_34_1","volume-title":"Handbook of Logic in Computer Science.","author":"MEINKE K."},{"key":"e_1_2_1_35_1","first-page":"459","article-title":"Initiality, induction and computability. In Algebraic Methods in Semantics, M. Nivat and J. C. Reynolds, Eds. Cambridge University Press, Cambridge","author":"MESEGUER J.","year":"1985","journal-title":"U.K."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(92)90155-O"},{"key":"e_1_2_1_38_1","first-page":"269","volume-title":"Proceedings of the 19th A CM Symposium on Principles of Programming Languages. ACM","author":"NIRKHE V.","year":"1992"},{"key":"e_1_2_1_39_1","first-page":"43","volume-title":"Proceedings of the 20th A CM Symposium on Principles of Programming Languages. ACM","author":"ODERSKY M.","year":"1993"},{"key":"e_1_2_1_40_1","unstructured":"PEYTON JONES S. L. 1987. The Implementation of Functional Programming Languages. Prentice Hall International Englewood Cliffs N.J. PEYTON JONES S. L. 1987. The Implementation of Functional Programming Languages. Prentice Hall International Englewood Cliffs N.J."},{"key":"e_1_2_1_41_1","doi-asserted-by":"crossref","first-page":"2","DOI":"10.2307\/2272645","article-title":"The ~-calculus is or-incomplete","volume":"39","author":"PLOTKIN G. D.","year":"1974","journal-title":"J. Symbol. Logic"},{"key":"e_1_2_1_43_1","first-page":"12","volume-title":"Proceedings of the 16th ACM Symposium on Principles of Programming Languages. ACM","author":"SELKE R. P.","year":"1989"},{"key":"e_1_2_1_45_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 5th A CM Conference on Functional Programming Languages and Computer Architecture","author":"SWARUP V."},{"key":"e_1_2_1_46_1","doi-asserted-by":"crossref","unstructured":"VAN DEURSEN A. HEERING J. AND KLINT P. Eds. 1996. Language Prototyping: An Algebraic Specification Approach. AMAST Series in Computing. World Scientific Singapore. VAN DEURSEN A. HEERING J. AND KLINT P. Eds. 1996. Language Prototyping: An Algebraic Specification Approach. AMAST Series in Computing. World Scientific Singapore.","DOI":"10.1142\/3163"},{"key":"e_1_2_1_47_1","volume-title":"Proceedings of the 5th IEEE Symposium on Logic in Computer Science. IEEE","author":"WAND M.","year":"1990"},{"key":"e_1_2_1_48_1","first-page":"297","volume-title":"Proceedings of the 21st ACM Symposium on Principles of Programming Languages. ACM","author":"WEISE D.","year":"1994"},{"key":"e_1_2_1_49_1","first-page":"675","article-title":"Algebraic specification. In Handbook of Theoretical Computer Science. Vol. B, Formal Models and Semantics, J. van Leeuwen, Ed. Elsevier\/The MIT Press","author":"WIRSING M.","year":"1990","journal-title":"Amsterdam"},{"key":"e_1_2_1_51_1","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1145\/99277.99290","volume-title":"Proceedings of the gth A CM SIGSOFT Symposium on Software Development Environments. ACM","author":"YANG W.","year":"1990"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/265943.265944","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,30]],"date-time":"2022-12-30T18:32:44Z","timestamp":1672425164000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/265943.265944"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997,9]]},"references-count":44,"journal-issue":{"issue":"5","published-print":{"date-parts":[[1997,9]]}},"alternative-id":["10.1145\/265943.265944"],"URL":"https:\/\/doi.org\/10.1145\/265943.265944","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[1997,9]]},"assertion":[{"value":"1997-09-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}