💾 Archived View for dcreager.net › papers › Gateley2005.gmi captured on 2024-02-05 at 10:06:14. Gemini links have been rewritten to link to archived content
⬅️ Previous capture (2023-07-22)
-=-=-=-=-=-=-
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.
Since it is unsound to reason about call-by-value languages using call-by name equational theories, we present two by-value combinatory logics and translations from the λ-value (λv) calculus to the logics. The first by-value logic is constructed in a manner similar to the λv-calculus: it is based on the byname combinatory logic, but the combinators are strict. The translation is non-standard to account for the strictness of the input program. The second by-value logic introduces laziness to K terms so that the translation can preserve the structure of functions that do not use their argument. Both logics include constants and delta rules, and we prove their equivalence with the λv-calculus.