Classical By-Need

DOI10.1007/978-3-662-49498-1_24zbMath1335.68034MaRDI QIDQ2802497

Alexis Saurin, Pierre-Marie Pédrot

Publication date: 26 April 2016

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-662-49498-1_24

zbMATH Keywords

linear logic; lazy evaluation; classical logic; lambda-calculus; control operators; call-by-need; linear head reduction; Krivine abstract machine; lambda-mu-calculus; sigma equivalence

Mathematics Subject Classification ID

68N18: Functional programming and lambda calculus

03B70: Logic in computer science

03F52: Proof-theoretic aspects of linear logic and other substructural logics

03B40: Combinatory logic and lambda calculus

Related Items

Unnamed Item, Unnamed Item, Unnamed Item, Taylor expansion, finiteness and strategies

Cites Work

• Unnamed Item
• Linear logic
• The lambda calculus. Its syntax and semantics. Rev. ed.
• An equivalence between lambda- terms
• On full abstraction for PCF: I, II and III
• A call-by-name lambda-calculus machine
• (Leftmost-Outermost) Beta Reduction is Invariant, Indeed
• Distilling abstract machines
• The Permutative λ-Calculus
• The Call-by-Need Lambda Calculus, Revisited
• Classical Call-by-Need Sequent Calculi: The Unity of Semantic Artifacts
• The duality of computation
• Classical Call-by-Need and Duality
• Defunctionalized Interpreters for Call-by-Need Evaluation
• The Structural λ-Calculus
• The call-by-need lambda calculus
• Classical logic, continuation semantics and abstract machines
• The call-by-need lambda calculus
• Explicit substitutions
• A nonstandard standardization theorem