Proof nets and the call-by-value -calculus

DOI10.1016/J.TCS.2015.08.006zbMATH Open1332.68026arXiv1303.7326OpenAlexW1136297157MaRDI QIDQ897928FDOQ897928

Beniamino Accattoli

Publication date: 8 December 2015

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

Abstract: This paper gives a detailed account of the relationship between (a variant of) the call-by-value lambda calculus and linear logic proof nets. The presentation is carefully tuned in order to realize a strong bisimulation between the two systems: every single rewriting step on the calculus maps to a single step on the nets, and viceversa. In this way, we obtain an algebraic reformulation of proof nets. Moreover, we provide a simple correctness criterion for our proof nets, which employ boxes in an unusual way.

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

Recommendations

• scientific article; zbMATH DE number 7356671
• scientific article; zbMATH DE number 2134911
• Proof nets and the linear substitution calculus
• An Operational Account of Call-by-Value Minimal and Classical λ-Calculus in “Natural Deduction” Form
• Intuitionistic differential nets and lambda-calculus

zbMATH Keywords

linear logicCurry-Howard isomorphismproof netscorrectness criteriaexplicit substitutionscall-by-value \(\lambda\)-calculusgraphical syntaxes

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (15)

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• On reduction and normalization in the computational core
• Title not available (Why is that?)
• Title not available (Why is that?)
• Strong call-by-value and multi types
• Title not available (Why is that?)
• A Fresh Look at the λ-Calculus
• Jumping Boxes
• Proof nets and the call-by-value \(\lambda\)-calculus
• Quantitative global memory
• A formal equational theory for call-by-push-value
• Light genericity
• Open Call-by-Value

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

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