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

DOI10.1007/S10990-006-0480-6zbMATH Open1112.68025OpenAlexW2028012052MaRDI QIDQ857915FDOQ857915

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)

Cites Work

• Call-by-name, call-by-value and the \(\lambda\)-calculus
• LCF considered as a programming language
• Notions of computation and monads
• Title not available (Why is that?)
• Title not available (Why is that?)
• The lambda calculus, its syntax and semantics
• Control categories and duality: On the categorical semantics of the lambda-mu calculus
• Classical logic, continuation semantics and abstract machines
• Operational reasoning for functions with local state
• Intensional interpretations of functionals of finite type I
• Title not available (Why is that?)
• Title not available (Why is that?)
• A fully abstract semantics for a higher-order functional language with nondeterministic computation
• Inductive, coinductive, and pointed types
• Adjunction models for call-by-push-value with stacks
• Jumbo λ-Calculus
• Title not available (Why is that?)
• Thunks and the λ-calculus
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (33)

• Focused linear logic and the \(\lambda\)-calculus
• Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types
• Title not available (Why is that?)
• On the relations between monadic semantics
• Galois connecting call-by-value and call-by-name
• The polarized \(\lambda\)-calculus
• Streams of approximations, equivalence of recursive effectful programs
• Polarized games
• Title not available (Why is that?)
• Polarized subtyping
• A faithful and quantitative notion of distant reduction for the lambda-calculus with generalized applications
• Amb Breaks Well-Pointedness, Ground Amb Doesn't
• Quantitative logics for equivalence of effectful programs
• Taylor expansion, finiteness and strategies
• Plotkin's call-by-value \(\lambda\)-calculus as a modal calculus
• A coherent differential PCF
• Title not available (Why is that?)
• Call-by-value combinatory logic and the lambda-value calculus
• Factorization in call-by-name and call-by-value calculi via linear logic
• Higher order functions and Brouwer’s thesis
• Infinite trace equivalence
• Title not available (Why is that?)
• The bang calculus revisited
• Iteration and labelled iteration
• Title not available (Why is that?)
• The bang calculus revisited
• Call-by-value is dual to call-by-name
• Title not available (Why is that?)
• Realisability semantics of parametric polymorphism, general references and recursive types
• Latent Effects for Reusable Language Components
• Title not available (Why is that?)
• Title not available (Why is that?)
• Implementing open call-by-value

   Recommendations

• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Adjunction models for call-by-push-value with stacks 👍 👎
• Call-by-value is dual to call-by-name 👍 👎
• Title not available (Why is that?) 👍 👎

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q857915)