×

Fully abstract translations between functional languages. (English) Zbl 0802.68023

Summary: 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 ‘functional translation’ that captures the essence of the proofs of full abstraction, and show that some languages cannot be translated into others.

MSC:

68N15 Theory of programming languages
68Q55 Semantics in the theory of computing
03B40 Combinatory logic and lambda calculus
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Moggi, Information and Control 93 pp 55– (1991)
[2] DOI: 10.1016/0304-3975(75)90017-1 · Zbl 0325.68006 · doi:10.1016/0304-3975(75)90017-1
[3] Felleisen, Springer-Verlag Lecture Notes in Computer Science 432 pp 134– (1990) · doi:10.1007/3-540-52592-0_60
[4] DOI: 10.1016/S0019-9958(85)80001-2 · Zbl 0594.03006 · doi:10.1016/S0019-9958(85)80001-2
[5] Bloom, Proc. Conf. Algebraic Methodology and Software Technology pp 133– (1989)
[6] DOI: 10.1016/0304-3975(79)90007-0 · Zbl 0411.03050 · doi:10.1016/0304-3975(79)90007-0
[7] DOI: 10.1016/0890-5401(90)90064-O · Zbl 0825.68447 · doi:10.1016/0890-5401(90)90064-O
[8] Barendregt, Studies in Logic 103 (1981)
[9] Abramsky, Research Topics in Functional Programming pp 65– (1990)
[10] Scott, A type theoretical alternative to CUCH, 1SWIM, OWHY (1969)
[11] Schwichtenberg, The L.E.J. Brouwer Centenary Symposium pp 453– (1982) · doi:10.1016/S0049-237X(09)70143-0
[12] Mitchell, Handbook of Theoretical Computer Science B pp 365– (1990)
[13] DOI: 10.1016/0304-3975(77)90053-6 · Zbl 0386.03006 · doi:10.1016/0304-3975(77)90053-6
[14] Gunter, Handbook of Theoretical Computer Science B pp 633– (1990)
[15] Gunter, Semantics of Programming Languages: Structures and Techniques (1992) · Zbl 0823.68059
[16] Sazonov, Algebra i Logika 15 pp 308– (1976) · Zbl 0415.03011 · doi:10.1007/BF01876321
[17] Plotkin, Notes on completeness of the full continuous type hierarchy (1982)
[18] Plotkin, A structural approach to operational semantics (1981)
[19] DOI: 10.1016/0304-3975(77)90044-5 · Zbl 0369.68006 · doi:10.1016/0304-3975(77)90044-5
[20] Friedman, Springer-Verlag Lecture Notes in Math 453 pp 22– (1975)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.