Call-by-push-value: Decomposing call-by-value and call-by-name

DOI10.1007/S10990-006-0480-6zbMath1112.68025OpenAlexW2028012052MaRDI QIDQ857915

Paul Blain Levy

Publication date: 5 January 2007

Published in: Higher-Order and Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10990-006-0480-6

zbMATH Keywords

Lambda-calculusMonadCall-by-nameCall-by-push-valueCall-by-valueComputational effect

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items (27)

Taylor expansion, finiteness and strategies ⋮ Quantitative logics for equivalence of effectful programs ⋮ Polarized games ⋮ Plotkin's call-by-value \(\lambda\)-calculus as a modal calculus ⋮ On the relations between monadic semantics ⋮ Streams of approximations, equivalence of recursive effectful programs ⋮ Galois connecting call-by-value and call-by-name ⋮ Polarized subtyping ⋮ A coherent differential PCF ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Focused linear logic and the \(\lambda\)-calculus ⋮ Factorization in call-by-name and call-by-value calculi via linear logic ⋮ Iteration and labelled iteration ⋮ The polarized \(\lambda\)-calculus ⋮ Infinite trace equivalence ⋮ Realisability semantics of parametric polymorphism, general references and recursive types ⋮ Unnamed Item ⋮ The bang calculus revisited ⋮ Unnamed Item ⋮ The bang calculus revisited ⋮ Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Higher order functions and Brouwer’s thesis ⋮ Amb Breaks Well-Pointedness, Ground Amb Doesn't

Cites Work

• Notions of computation and monads
• The lambda calculus, its syntax and semantics
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• LCF considered as a programming language
• A fully abstract semantics for a higher-order functional language with nondeterministic computation
• Control categories and duality: on the categorical semantics of the lambda-mu calculus
• Inductive, coinductive, and pointed types
• Adjunction Models For Call-By-Push-Value With Stacks
• Jumbo λ-Calculus
• Classical logic, continuation semantics and abstract machines
• Thunks and the λ-calculus
• Intensional interpretations of functionals of finite type I
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Call-by-push-value: Decomposing call-by-value and call-by-name