Proof nets and the call-by-value \(\lambda\)-calculus

DOI10.1016/J.TCS.2015.08.006zbMath1332.68026arXiv1303.7326OpenAlexW1136297157MaRDI QIDQ897928

Beniamino Accattoli

Publication date: 8 December 2015

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1303.7326

zbMATH Keywords

linear logicproof netsCurry-Howard isomorphismexplicit substitutionscorrectness criteriacall-by-value \(\lambda\)-calculusgraphical syntaxes

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Combinatory logic and lambda calculus (03B40)

Related Items (8)

Open Call-by-Value ⋮ Proof nets and the call-by-value \(\lambda\)-calculus ⋮ Quantitative global memory ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A Fresh Look at the λ-Calculus ⋮ On reduction and normalization in the computational core

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Intuitionistic differential nets and lambda-calculus
• Linear logic
• Resource operators for \(\lambda\)-calculus
• Proof nets and the call-by-value \(\lambda\)-calculus
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• An equivalence between lambda- terms
• Reversible, irreversible and optimal \(\lambda\)-machines
• Call-by-name, call-by-value, call-by-need and the linear lambda calculus
• Polarized proof-nets and \(\lambda \mu\)-calculus
• The differential \(\lambda \mu\)-calculus
• Distilling abstract machines
• Call-by-Value Solvability, Revisited
• On the Value of Variables
• Linear Logic and Strong Normalization
• The Prismoid of Resources
• The Structural λ-Calculus
• Encoding Strategies in the Lambda Calculus with Interaction Nets
• An Operational Account of Call-by-Value Minimal and Classical λ-Calculus in “Natural Deduction” Form
• Jumping Boxes
• Confluence of Pure Differential Nets with Promotion
• Beta reduction is invariant, indeed
• The call-by-value λ-calculus: a semantic investigation
• Proof nets and explicit substitutions
• Call-by-value Solvability
• A Semantical and Operational Account of Call-by-Value Solvability
• Automated Deduction – CADE-19
• Rewriting Techniques and Applications

This page was built for publication: Proof nets and the call-by-value \(\lambda\)-calculus