Call-by-value is dual to call-by-name

DOI10.1145/944705.944723MaRDI QIDQ5261275zbMATH OpenOpenAlexFDO

Authors Philip Wadler

Publication date 2 July 2015

Published in Proceedings of the eighth ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/944705.944723

zbMATH Keywords

Curry-Howard correspondencelogicnatural deductionlambda calculussequent calculuslambda-mu calculusDe Morgan dual

Mathematics Subject Classification ID

Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Recommendations

• Call-by-Value Is Dual to Call-by-Name, Extended
• Term Rewriting and Applications
• scientific article; zbMATH DE number 1086682
• scientific article; zbMATH DE number 1948183
• Call-by-push-value: Decomposing call-by-value and call-by-name
• scientific article; zbMATH DE number 1456965
• Call-by-Name and Call-by-Value in Normal Modal Logic
• Call-By-Value, Again!
• scientific article; zbMATH DE number 512793
• A reflection on call-by-value

Cited in

(36)

• Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage
• Galois connecting call-by-value and call-by-name
• On the computational representation of classical logical connectives
• Classical Logic with Mendler Induction
• scientific article; zbMATH DE number 7447733 (Why is no real title available?)
• scientific article; zbMATH DE number 7713500 (Why is no real title available?)
• Strong normalization of classical natural deduction with disjunctions
• Focalisation and Classical Realisability
• PML2: integrated program verification in ML
• Call-by-Value Is Dual to Call-by-Name, Extended
• Call-by-Name and Call-by-Value in Normal Modal Logic
• Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\)
• On the unity of duality
• Intuitionistic Letcc via Labelled Deduction
• scientific article; zbMATH DE number 1948183 (Why is no real title available?)
• Normalization in the simply typed -calculus
• Dual Calculus with Inductive and Coinductive Types
• The duality of computation
• Abstracting models of strong normalization for classical calculi
• A classical sequent calculus with dependent types
• Call-by-push-value: Decomposing call-by-value and call-by-name
• Call-by-value and call-by-name dual calculi with inductive and coinductive types
• Categorical proof theory of classical propositional calculus
• Classical call-by-need and duality
• A Survey of the Proof-Theoretic Foundations of Logic Programming
• Proofs, tests and continuation passing style
• Investigations on the dual calculus
• scientific article; zbMATH DE number 7243675 (Why is no real title available?)
• Call-by-name reduction and cut-elimination in classical logic
• Term Rewriting and Applications
• Linear \(\lambda \mu\) is CP (more or less)
• CPS-translation as adjoint
• Call-by-value combinatory logic and the lambda-value calculus
• Classical (co)recursion: Mechanics
• Classical \(F_{\omega}\), orthogonality and symmetric candidates
• scientific article; zbMATH DE number 7533346 (Why is no real title available?)

This page was built for publication: Call-by-value is dual to call-by-name

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