{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:24:31Z","timestamp":1761611071808},"reference-count":28,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[1992,11,1]],"date-time":"1992-11-01T00:00:00Z","timestamp":720576000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":7563,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[1992,11]]},"DOI":"10.1016\/0304-3975(92)90301-u","type":"journal-article","created":{"date-parts":[[2002,7,26]],"date-time":"2002-07-26T03:47:37Z","timestamp":1027655257000},"page":"167-215","source":"Crossref","is-referenced-by-count":16,"title":["Inferring the equivalence of functional programs that mutate data"],"prefix":"10.1016","volume":"105","author":[{"given":"Ian","family":"Mason","sequence":"first","affiliation":[]},{"given":"Carolyn","family":"Talcott","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/0304-3975(92)90301-U_BIB1","series-title":"Solvable Cases of the Decision Problem","author":"Ackermann","year":"1954"},{"key":"10.1016\/0304-3975(92)90301-U_BIB2","series-title":"Current Trends in Hardware Verification","first-page":"323","article-title":"An overview of the Edinburgh logical framework","author":"Avron","year":"1989"},{"issue":"4","key":"10.1016\/0304-3975(92)90301-U_BIB3","doi-asserted-by":"crossref","first-page":"637","DOI":"10.1145\/4472.4474","article-title":"Side effects and aliasing can have simple axiomatic descriptions","volume":"7","author":"Boehm","year":"1985","journal-title":"ACM TOPLAS"},{"key":"10.1016\/0304-3975(92)90301-U_BIB4","series-title":"A Computational Logic","author":"Boyer","year":"1979"},{"key":"10.1016\/0304-3975(92)90301-U_BIB5","series-title":"Model Theory","author":"Chang","year":"1973"},{"key":"10.1016\/0304-3975(92)90301-U_BIB6","first-page":"59","article-title":"Making variables abstract: an equational theory for Russell","author":"Demers","year":"1983","journal-title":"Proc. 10th ACM Symp. on Principles of Programming Languages"},{"key":"10.1016\/0304-3975(92)90301-U_BIB7","series-title":"Ph.D. Thesis","article-title":"The calcului of lambda-v-cs conversion: a syntactic theory of control and state in imperative higher-order programming languages","author":"Felleisen","year":"1987"},{"key":"10.1016\/0304-3975(92)90301-U_BIB8","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1145\/62678.62686","article-title":"\u03bb-v-cs: an extended \u03bb-calculus for scheme","volume":"Vol. 52","author":"Felleisen","year":"1988","journal-title":"Proc. 1988 ACM Conf. on Lisp and functional programming"},{"key":"10.1016\/0304-3975(92)90301-U_BIB9","series-title":"Tech. Report COMP TR89-100","article-title":"The revised report on the syntactic theories of sequential control and state","author":"Felleisen","year":"1989"},{"key":"10.1016\/0304-3975(92)90301-U_BIB10","series-title":"Proc. 2nd Ann. Symp. on Logic in Computer Science","first-page":"194","article-title":"A framework for defining logics","author":"Harper","year":"1987"},{"key":"10.1016\/0304-3975(92)90301-U_BIB11","series-title":"Ph.D. Thesis","article-title":"Types and effects, towards the integration of functional and imperative programming","author":"Lucassen","year":"1987"},{"key":"10.1016\/0304-3975(92)90301-U_BIB12","first-page":"47","article-title":"Polymorphic effect systems","author":"Lucassen","year":"1988","journal-title":"Conf. Record of the 16th Ann. ACM Symp. on Principles of Programming Languages"},{"key":"10.1016\/0304-3975(92)90301-U_BIB13","series-title":"Proc. 1st Ann. Symp. on Logic in Computer Science","first-page":"105","article-title":"Equivalence of first order Lisp programs: proving properties of destructive programs via transformation","author":"Mason","year":"1986"},{"key":"10.1016\/0304-3975(92)90301-U_BIB14_1","series-title":"Ph.D. Thesis","article-title":"The semantics of destructive Lisp","author":"Mason","year":"1986"},{"key":"10.1016\/0304-3975(92)90301-U_BIB14_2","unstructured":"also available as CSLI Lecture Notes, Vol. 5, Center the Study of Language and Information, Stanford University."},{"key":"10.1016\/0304-3975(92)90301-U_BIB15","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/0167-6423(88)90026-3","article-title":"Verification of programs that destructively manipulate data","volume":"10","author":"Mason","year":"1988","journal-title":"Sci. Comput. Programming"},{"key":"10.1016\/0304-3975(92)90301-U_BIB16","series-title":"Tech. Report STAN-CS-85-1057","article-title":"Memories of S-expressions: proving properties of Lisp-like programs that destructively alter memory","author":"Mason","year":"1985"},{"key":"10.1016\/0304-3975(92)90301-U_BIB17","series-title":"Proc. 16th EATCS Coll. on Automata, Languages, and Programming, Stresa","first-page":"574","article-title":"Programming transforming, and proving with function abstractions and memories","volume":"Vol. 372","author":"Mason","year":"1989"},{"key":"10.1016\/0304-3975(92)90301-U_BIB18","series-title":"Programming Language Implementation and Logic Programming, PLILP '90","first-page":"189","article-title":"Reasoning about programs with effects","volume":"Vol. 456","author":"Mason","year":"1990"},{"key":"10.1016\/0304-3975(92)90301-U_BIB19","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1017\/S0956796800000125","article-title":"Equivalence in functional languages with effects","volume":"1","author":"Mason","year":"1991","journal-title":"J. Funct. Programming"},{"key":"10.1016\/0304-3975(92)90301-U_BIB20","first-page":"297","article-title":"Program transformation for configuring components","author":"Mason","year":"1991","journal-title":"ACM\/IFIP Symp. on Partial Evaluation and Semantics based Program Manipulation"},{"key":"10.1016\/0304-3975(92)90301-U_BIB21","author":"Mason","year":"1991","journal-title":"Program transformation via constraint propagation"},{"key":"10.1016\/0304-3975(92)90301-U_BIB22","series-title":"Proc. 4th Ann. Symp. on Logic in Computer Science","first-page":"14","article-title":"Computational lambda-calculus and monads","author":"Moggi","year":"1989"},{"key":"10.1016\/0304-3975(92)90301-U_BIB23","series-title":"Ph.D. Thesis","article-title":"Lambda calculus models of programming languages","author":"Morris","year":"1968"},{"key":"10.1016\/0304-3975(92)90301-U_BIB24","series-title":"Proc. Semantics of Data Types, International Symp., Sophia-Antipolis","first-page":"97","article-title":"A basic abstract semantic algebra","volume":"Vol. 173","author":"Mosses","year":"1984"},{"key":"10.1016\/0304-3975(92)90301-U_BIB25","series-title":"Tech. Report STAN-CS-77-647","article-title":"Fast decision procedures based on congruence closure","author":"Nelson","year":"1977"},{"key":"10.1016\/0304-3975(92)90301-U_BIB26","series-title":"Tech. Report STAN-CS-78-678","article-title":"Reasoning about recursively defined data structures","author":"Oppen","year":"1978"},{"key":"10.1016\/0304-3975(92)90301-U_BIB27","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","article-title":"Call-by-name, call-by-value and the lambda-v-calculus","volume":"1","author":"Plotkin","year":"1975","journal-title":"Theoret. Comput. Sci."}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:030439759290301U?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:030439759290301U?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,13]],"date-time":"2019-04-13T04:20:48Z","timestamp":1555129248000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/030439759290301U"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,11]]},"references-count":28,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1992,11]]}},"alternative-id":["030439759290301U"],"URL":"https:\/\/doi.org\/10.1016\/0304-3975(92)90301-u","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[1992,11]]}}}