Classical Call-by-Need and Duality

DOI10.1007/978-3-642-21691-6_6zbMath1331.68041OpenAlexW184349421MaRDI QIDQ3007655

Alexis Saurin, Zena M. Ariola, Hugo Herbelin

Publication date: 17 June 2011

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-21691-6_6

zbMATH Keywords

controlsequent calculuslazy evaluationclassical logic\(\lambda \mu \)-calculuscall-by-needduality of computationsubtraction connective

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items

Unnamed Item, Unnamed Item, Classical By-Need, Abstracting models of strong normalization for classical calculi, Unnamed Item, Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The parametric lambda calculus. A metamodel for computation.
• The lambda calculus. Its syntax and semantics. Rev. ed.
• A concurrent lambda calculus with futures
• A type-theoretic foundation of delimited continuations
• A syntactic theory of sequential control
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• A set of postulates for the foundation of logic
• A proof-theoretic foundation of abortive continuations
• Control categories and duality: on the categorical semantics of the lambda-mu calculus
• λμ-calculus and Böhm's theorem
• The duality of computation
• Control reduction theories: the benefit of structural substitution
• Defunctionalized Interpreters for Call-by-Need Evaluation
• An Operational Account of Call-by-Value Minimal and Classical λ-Calculus in “Natural Deduction” Form
• The call-by-need lambda calculus
• The call-by-need lambda calculus
• A new deconstructive logic: linear logic
• Lambda terms for natural deduction, sequent calculus and cut elimination
• Lazy evaluation and delimited control
• Subtractive logic