{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:53:03Z","timestamp":1776891183410,"version":"3.51.2"},"reference-count":43,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","issue":"3","license":[{"start":{"date-parts":[[2008,11,7]],"date-time":"2008-11-07T00:00:00Z","timestamp":1226016000000},"content-version":"unspecified","delay-in-days":6339,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[1991,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Traditionally the view has been that direct expression of control and store mechanisms and clear mathematical semantics are incompatible requirements. This paper shows that adding objects with memory to the call-by-value lambda calculus results in a language with a rich equational theory, satisfying many of the usual laws. Combined with other recent work, this provides evidence that expressive, mathematically clean programming languages are indeed possible.<\/jats:p>","DOI":"10.1017\/s0956796800000125","type":"journal-article","created":{"date-parts":[[2008,11,7]],"date-time":"2008-11-07T11:14:35Z","timestamp":1226056475000},"page":"287-327","source":"Crossref","is-referenced-by-count":106,"title":["Equivalence in functional languages with effects"],"prefix":"10.46298","volume":"1","author":[{"given":"Ian","family":"Mason","sequence":"first","affiliation":[]},{"given":"Carolyn","family":"Talcott","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2008,11,7]]},"reference":[{"key":"S0956796800000125_ref006","article-title":"A theory of variable types","volume":"19","author":"Feferman","year":"1985","journal-title":"Revista Colombiana de Mat\u00e9maticas"},{"key":"S0956796800000125_ref010","unstructured":"Guzm\u00e1n J. C. and Hudak P. 1990. Single-threaded polymorphic lambda calculus. In Fifth Ann. Symposium on Logic in Computer Science.IEEE Press."},{"key":"S0956796800000125_ref011","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(77)90033-9"},{"key":"S0956796800000125_ref016","doi-asserted-by":"crossref","unstructured":"Lucassen J. M. and Gifford D. K. 1988. Polymorphic effect systems. In Conf. record 16th Ann. ACM symposium on principles of programming languages, 47\u201357, ACM.","DOI":"10.1145\/73560.73564"},{"key":"S0956796800000125_ref026","volume-title":"Programming Language Implementation and Logic Programming, PLILP'90","volume":"456","author":"Mason","year":"1990"},{"key":"S0956796800000125_ref002","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/1086.001.0001","volume-title":"Actors: A Model of Concurrent Computation in Distributed Systems","author":"Agha","year":"1986"},{"key":"S0956796800000125_ref031","volume-title":"Fast decision procedures based on congruence closure","author":"Nelson","year":"1977"},{"key":"S0956796800000125_ref037","unstructured":"Smith S. F. From operational to denotational semantics. Technical Report 89-12, Department of Computer Science, The Johns Hopkins University, USA. To appear in the Proceedings of the 7th Conference on the Mathematical Foundations of Programming Semantics,MFPS91 LNCS Springer Verlag."},{"key":"S0956796800000125_ref004","doi-asserted-by":"publisher","DOI":"10.1145\/4472.4474"},{"key":"S0956796800000125_ref027","unstructured":"Moggi E. 1989. Computational lambda-calculus and monads. In Fourth Ann. Symposium on Logic in Computer Science.IEEE Press."},{"key":"S0956796800000125_ref024","unstructured":"Mason I. A. and Talcott C. L. Program transformation for configuring components. To appear (b) ACM Sigplan Symposium on Partial Evaluation and Semantics Based Program Manipulation. PEPM91."},{"key":"S0956796800000125_ref013","doi-asserted-by":"publisher","DOI":"10.21236\/AD0406138"},{"key":"S0956796800000125_ref034","volume-title":"Assignments for applicative languages","author":"Reddy","year":"1990"},{"key":"S0956796800000125_ref005","doi-asserted-by":"crossref","unstructured":"Demers A. and Donahue J. 1983. Making variables abstract: an equational theory for Russell. In 10th ACM Symposium on Principles of Programming Languages,ACM.","DOI":"10.1145\/567067.567075"},{"key":"S0956796800000125_ref003","volume-title":"The lambda calculus: its syntax and semantics","author":"Barendregt","year":"1981"},{"key":"S0956796800000125_ref017","unstructured":"Mason I. A. 1986. The Semantics of Destructive Lisp. PhD thesis, Stanford University, USA."},{"key":"S0956796800000125_ref012","unstructured":"Howe D. 1989. Equality in the lazy lambda calculus. In Fourth Ann. Symposium on Logic in Computer Science.IEEE Press."},{"key":"S0956796800000125_ref008","unstructured":"Felleisen M. 1987. The Calcului of Lambda-v-cs Conversion: A Syntactic Theory of Control and State in Imperative Higher-order Programming Languages. PhD thesis, Indiana University, USA."},{"key":"S0956796800000125_ref019","unstructured":"Mason I. A. and Talcott C. L. 1989 a. Axiomatizing operational equivalence in the presence of side effects. In Fourth Ann. Symposium on Logic in Computer Science.IEEE Press."},{"key":"S0956796800000125_ref025","unstructured":"Mason I. A. and Talcott C. L. Program transformation via constraint propagation. To appear (c)."},{"key":"S0956796800000125_ref009","unstructured":"Felleisen M. and Hieb R. 1989. The revised report on the syntactic theories of sequential control and state. Technical Report COMP TR89-100, Rice University, USA."},{"key":"S0956796800000125_ref014","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/6.4.308"},{"key":"S0956796800000125_ref022","unstructured":"Mason I. A. and Talcott C. L. Inferring the equivalence of functional programs that mutate data. To appear (a) in Theor. Comput. Sci."},{"key":"S0956796800000125_ref015","unstructured":"Lucassen J. M. 1987. Types and Effects, towards the integration of functional and imperative programming. PhD thesis, MIT, USA."},{"key":"S0956796800000125_ref020","volume-title":"Proc. 16th EATCS Colloquium on Automata, Languages, and Programming, Stresa","volume":"372","author":"Mason","year":"1989"},{"key":"S0956796800000125_ref039","unstructured":"Talcott C. L. 1985. The Essence of Rum: A Theory of the Intensional and Extensional Aspects of Lisp-Type Computation. PhD thesis, Stanford University, USA."},{"key":"S0956796800000125_ref021","volume-title":"A sound and complete axiomatization of operational equivalence between programs with memory","author":"Mason","year":"1989"},{"key":"S0956796800000125_ref029","unstructured":"Morris J. H. 1968. Lambda calculus models of programming languages. PhD thesis, Massachusetts Institute of Technology, USA."},{"key":"S0956796800000125_ref001","volume-title":"Research Topics in Functional Programming","author":"Abramsky","year":"1990"},{"key":"S0956796800000125_ref023","unstructured":"Mason I. A. and Talcott C. L. Syntactic semantics. In preparation."},{"key":"S0956796800000125_ref028","volume-title":"Laboratory for foundations of computer science","author":"Moggi","year":"1990"},{"key":"S0956796800000125_ref030","volume-title":"Semantics of data types, international symposium","volume":"173","author":"Mosses","year":"1984"},{"key":"S0956796800000125_ref032","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512776"},{"key":"S0956796800000125_ref033","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"S0956796800000125_ref035","volume-title":"Proc. ACM Nat. Convention","author":"Reynolds","year":"1972"},{"key":"S0956796800000125_ref038","volume-title":"Scheme, an interpreter for extended lambda calculus","author":"Steele","year":"1975"},{"key":"S0956796800000125_ref040","doi-asserted-by":"publisher","DOI":"10.21236\/ADA324006"},{"key":"S0956796800000125_ref041","volume-title":"Design and Implementation of Symbolic Computation Systems, DISCO'90","volume":"429","author":"Talcott","year":"1990"},{"key":"S0956796800000125_ref042","volume-title":"IFIP Working Conf. Programming Concepts and Methods","author":"Wadler","year":"1990"},{"key":"S0956796800000125_ref018","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(88)90026-3"},{"key":"S0956796800000125_ref043","volume-title":"ABCL: An Object-Oriented Concurrent System","author":"Yonezawa","year":"1990"},{"key":"S0956796800000125_ref036","doi-asserted-by":"crossref","unstructured":"Reynolds J. C. 1989. Syntactic control of interference, II. Proc. 16th EATCS Colloquium on Automata, Languages, and Programming, Stresa, Italy. Volume 372 of Lecture Notes in Computer Science, Springer-Verlag.","DOI":"10.1007\/BFb0035793"},{"key":"S0956796800000125_ref007","volume-title":"Logic and Computation (vol. 104) Contemporary Mathematics","author":"Feferman","year":"1990"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796800000125","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:17:48Z","timestamp":1776889068000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796800000125\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991,7]]},"references-count":43,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1991,7]]}},"alternative-id":["S0956796800000125"],"URL":"https:\/\/doi.org\/10.1017\/s0956796800000125","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[1991,7]]}}}