{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:27:20Z","timestamp":1761611240962},"reference-count":38,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T00:00:00Z","timestamp":1236124800000},"content-version":"unspecified","delay-in-days":5572,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[1993,12]]},"abstract":"<jats:p>We examine the problem of finding fully abstract translations between programming languages, i.e., translations that preserve code equivalence and nonequivalence. We present three examples of fully abstract translations: one from call-by-value to lazy PCF, one from call-by-name to call-by-value PCF, and one from lazy to call-by-value PCF. The translations yield lower bounds on decision procedures for proving equivalences of code. We define a notion of \u2018functional translation\u2019 that captures the essence of the proofs of full abstraction, and show that some languages <jats:italic>cannot<\/jats:italic> be translated into others.<\/jats:p>","DOI":"10.1017\/s0960129500000293","type":"journal-article","created":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T09:01:36Z","timestamp":1236157296000},"page":"387-415","source":"Crossref","is-referenced-by-count":13,"title":["Fully abstract translations between functional languages"],"prefix":"10.1017","volume":"3","author":[{"given":"Jon G.","family":"Riecke","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2009,3,4]]},"reference":[{"key":"S0960129500000293_ref029","doi-asserted-by":"publisher","DOI":"10.1007\/BF01876321"},{"key":"S0960129500000293_ref028","unstructured":"Riecke J. G. (1991b) The Logic and Expressibility of Simply-Typed Call-by-Value and Lazy Languages, PhD thesis, Massachusetts Institute of Technology. (Available as technical report MIT\/LCS\/TR-523, MIT Laboratory for Computer Science.)"},{"key":"S0960129500000293_ref018","unstructured":"Moggi E. (1988) The Partial Lambda Calculus, PhD thesis, University of Edinburgh."},{"key":"S0960129500000293_ref031","volume-title":"A type theoretical alternative to CUCH, 1SWIM, OWHY","author":"Scott","year":"1969"},{"key":"S0960129500000293_ref026","volume-title":"Notes on completeness of the full continuous type hierarchy","author":"Plotkin","year":"1982"},{"key":"S0960129500000293_ref007","unstructured":"Despeyroux J. (1986) Proof of translation in natural semantics. Proceedings, Symposium on Logic in Computer Science, IEEE 193\u2013205."},{"key":"S0960129500000293_ref025","volume-title":"A structural approach to operational semantics","author":"Plotkin","year":"1981"},{"key":"S0960129500000293_ref024","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"S0960129500000293_ref022","unstructured":"Ong C.-H. L. (1988b) The Lazy Lambda Calculus: An Investigation into the Foundations of Functional Programming, PhD thesis, Imperial College, University of London."},{"key":"S0960129500000293_ref004","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90064-O"},{"key":"S0960129500000293_ref021","doi-asserted-by":"crossref","unstructured":"Ong C.-H. L. (1988a) Fully abstract models of the lazy lambda calculus. 29th Annual Symposium on Foundations of Computer Science, IEEE 368\u2013376.","DOI":"10.1109\/SFCS.1988.21953"},{"key":"S0960129500000293_ref017","doi-asserted-by":"crossref","unstructured":"Mitchell J. C. (1991) On abstraction and the expressive power of programming languages. In: Theoretical Aspects of Computer Software. Springer-Verlag Lecture Notes in Computer Science (to appear).","DOI":"10.1007\/3-540-54415-1_51"},{"key":"S0960129500000293_ref033","doi-asserted-by":"crossref","unstructured":"Sieber K. (1990) Relating full abstraction results for different programming languages. In: Foundations of Software Technology and Theoretical Computer Science, Bangalore, India.","DOI":"10.1007\/3-540-53487-3_58"},{"key":"S0960129500000293_ref016","first-page":"365","volume-title":"Handbook of Theoretical Computer Science B","author":"Mitchell","year":"1990"},{"key":"S0960129500000293_ref014","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90053-6"},{"key":"S0960129500000293_ref012","doi-asserted-by":"crossref","unstructured":"Kahn G. (1987) Natural semantics. Proceedings, Symposium on Theoretical Aspects of Computer Science. Springer-Verlag Lecture Notes in Computer Science 247.","DOI":"10.1007\/BFb0039592"},{"key":"S0960129500000293_ref010","volume-title":"Semantics of Programming Languages: Structures and Techniques","author":"Gunter","year":"1992"},{"key":"S0960129500000293_ref006","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1990.113757"},{"key":"S0960129500000293_ref037","unstructured":"Stoughton A. (1988) Fully Abstract Models of Progamming Languages. Research Notes in Theoretical Computer Science, Pitman\/Wiley. (Revision of Ph.D thesis, Dept. of Computer Science, Univ. Edinburgh, Report No. CST-40\u201386, 1986.)"},{"key":"S0960129500000293_ref027","doi-asserted-by":"crossref","unstructured":"Riecke J. G. (1991a) Fully abstract translations between functional languages (preliminary report). Conference Record of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, ACM 245\u2013254.","DOI":"10.1145\/99583.99617"},{"key":"S0960129500000293_ref008","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52592-0_60"},{"key":"S0960129500000293_ref015","unstructured":"Mitchell J. C. (1986) Lisp is not universal (summary). Unpublished manuscript, AT&T Bell Laboratories."},{"key":"S0960129500000293_ref032","doi-asserted-by":"crossref","unstructured":"Shapiro E. (1991) Separating concurrent languages with categories of language embeddings. Proceedings of the Twenty-Third Annual ACM Symposium on Theory of Computing.","DOI":"10.1145\/103418.103423"},{"key":"S0960129500000293_ref019","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39155"},{"key":"S0960129500000293_ref013","unstructured":"Meyer A. R. (1988) Semantical paradigms: Notes for an invited lecture, with two appendices by Stavros S. Cosmadakis. In: Proceedings, Third Annual Symposium on Logic in Computer Science, IEEE 236\u2013255."},{"key":"S0960129500000293_ref009","first-page":"22","volume-title":"Springer-Verlag Lecture Notes in Math","volume":"453","author":"Friedman","year":"1975"},{"key":"S0960129500000293_ref011","first-page":"633","volume-title":"Handbook of Theoretical Computer Science B","author":"Gunter","year":"1990"},{"key":"S0960129500000293_ref001","first-page":"65","volume-title":"Research Topics in Functional Programming","author":"Abramsky","year":"1990"},{"key":"S0960129500000293_ref002","volume-title":"Studies in Logic","volume":"103","author":"Barendregt","year":"1981"},{"key":"S0960129500000293_ref034","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91626"},{"key":"S0960129500000293_ref035","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(79)90007-0"},{"key":"S0960129500000293_ref036","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(85)80001-2"},{"key":"S0960129500000293_ref023","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"S0960129500000293_ref005","first-page":"133","volume-title":"Proc. Conf. Algebraic Methodology and Software Technology","author":"Bloom","year":"1989"},{"key":"S0960129500000293_ref020","first-page":"55","article-title":"Notions of computation and monads","volume":"93","author":"Moggi","year":"1991","journal-title":"Information and Control"},{"key":"S0960129500000293_ref030","first-page":"453","volume-title":"The L.E.J. Brouwer Centenary Symposium","author":"Schwichtenberg","year":"1982"},{"key":"S0960129500000293_ref003","unstructured":"Bloom B. (1988) Can LCF be topped? In: Proceedings, Third Annual Symposium on Logic in Computer Science, IEEE 282\u2013295."},{"key":"S0960129500000293_ref038","doi-asserted-by":"crossref","unstructured":"Thomsen B. (1989) A calculus of higher order communicating systems. Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, ACM 143\u2013154.","DOI":"10.1145\/75277.75290"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129500000293","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T20:54:46Z","timestamp":1557953686000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129500000293\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,12]]},"references-count":38,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1993,12]]}},"alternative-id":["S0960129500000293"],"URL":"https:\/\/doi.org\/10.1017\/s0960129500000293","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993,12]]}}}