Call-by-name, call-by-value, call-by-need and the linear lambda calculus

DOI10.1016/S0304-3975(98)00358-2zbMath0952.03009MaRDI QIDQ1575882

Philip Wadler, David N. Turner, J. Maraist, Martin Odersky

Publication date: 23 August 2000

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

Curry-Howard isomorphismaffine calculuscall-by-name calculuscall-by-value calculustranslations of intuitionistic logic into linear logic

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Combinatory logic and lambda calculus (03B40)

Related Items (25)

Plotkin's call-by-value \(\lambda\)-calculus as a modal calculus ⋮ Call-by-Value Non-determinism in a Linear Logic Type Discipline ⋮ Open Call-by-Value ⋮ Unnamed Item ⋮ A higher-order language for Markov kernels and linear operators ⋮ Proof nets and the call-by-value \(\lambda\)-calculus ⋮ Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic ⋮ Node Replication: Theory And Practice ⋮ The untyped computational \(\lambda \)-calculus and its intersection type discipline ⋮ Unnamed Item ⋮ Head reduction and normalization in a call-by-value lambda-calculus ⋮ Factorization in call-by-name and call-by-value calculi via linear logic ⋮ The spirit of node replication ⋮ The bang calculus revisited ⋮ Unnamed Item ⋮ Call-By-Push-Value from a Linear Logic Point of View ⋮ The bang calculus revisited ⋮ Reasoning About Call-by-need by Means of Types ⋮ A Fresh Look at the λ-Calculus ⋮ A Linear-Logical Reconstruction of Intuitionistic Modal Logic S4 ⋮ From parametric polymorphism to models of polymorphic FPC ⋮ An implementation model of the typed λ-calculus based on Linear Chemical Abstract Machine ⋮ On \(\Pi\)-conversion in the \(\lambda\)-cube and the combination with abbreviations ⋮ Proof nets, garbage, and computations ⋮ On reduction and normalization in the computational core

This page was built for publication: Call-by-name, call-by-value, call-by-need and the linear lambda calculus