PLS Lab

Untyped call-by-value \lambda-calculus

Please expand.

Call-by-value combinatory logic

It is well-known that there is a close correspondence between the untyped \lambda-calculus and combinatory logic. Somewhat surprisingly, this correspondence has been extended to the untyped call-by-value \lambda-calculus, and a corresponding "by value" combinatory logic by Gateley and Duba 1991.

See also

References

Plotkin, G.D. 1975. ‘Call-by-Name, Call-by-Value and the λ-Calculus’. Theoretical Computer Science 1 (2): 125–59. https://doi.org/10.1016/0304-3975(75)90017-1. pdf 
@article{plotkin_1975,
	title = {Call-by-name, call-by-value and the λ-calculus},
	volume = {1},
	doi = {10.1016/0304-3975(75)90017-1},
	number = {2},
	journal = {Theoretical Computer Science},
	author = {Plotkin, G.D.},
	year = {1975},
	pages = {125--159}
}
Gateley, J., Duba, B.F. (1992). Call-by-value combinatory logic and the lambda-value calculus. In: Brookes, S., Main, M., Melton, A., Mislove, M., Schmidt, D. (eds) Mathematical Foundations of Programming Semantics. MFPS 1991. Lecture Notes in Computer Science, vol 598. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55511-0_2