Fully abstract translations between functional languages
- 4 March 1993
- journal article
- research article
- Published by Cambridge University Press (CUP) in Mathematical Structures in Computer Science
- Vol. 3 (4) , 387-415
- https://doi.org/10.1017/s0960129500000293
Abstract
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.Keywords
This publication has 20 references indexed in Scilit:
- Natural semanticsPublished by Springer Nature ,2005
- Notions of computation and monadsInformation and Computation, 1991
- Can LCF be topped? Flat lattice models of typed λ-calculusInformation and Computation, 1990
- Logical relations and the typed λ-calculusInformation and Control, 1985
- Complexity of Normalization in the Pure Typed Lambda – CalculusPublished by Elsevier ,1982
- The typed λ-calculus is not elementary recursiveTheoretical Computer Science, 1979
- LCF considered as a programming languageTheoretical Computer Science, 1977
- Fully abstract models of typed λ-calculiTheoretical Computer Science, 1977
- Expressibility of functions in D. Scott's LCF languageAlgebra and Logic, 1976
- Call-by-name, call-by-value and the λ-calculusTheoretical Computer Science, 1975