Proof nets and the call-by-value -calculus
From MaRDI portal
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.
Recommendations
Cites work
- scientific article; zbMATH DE number 1342282 (Why is no real title available?)
- scientific article; zbMATH DE number 2016068 (Why is no real title available?)
- scientific article; zbMATH DE number 2134911 (Why is no real title available?)
- scientific article; zbMATH DE number 786499 (Why is no real title available?)
- A Semantical and Operational Account of Call-by-Value Solvability
- An Operational Account of Call-by-Value Minimal and Classical λ-Calculus in “Natural Deduction” Form
- An abstract factorization theorem for explicit substitutions
- An equivalence between lambda- terms
- Beta reduction is invariant, indeed
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- Call-by-name, call-by-value, call-by-need and the linear lambda calculus
- Call-by-value Solvability
- Call-by-value solvability, revisited
- Confluence of Pure Differential Nets with Promotion
- Distilling abstract machines
- Encoding Strategies in the Lambda Calculus with Interaction Nets
- Evaluating functions as processes
- Intuitionistic differential nets and lambda-calculus
- Jumping Boxes
- Labelled \(\lambda\)-calculi with explicit copy and erase
- Linear Logic and Strong Normalization
- Linear logic
- On the value of variables
- Polarized proof-nets and \(\lambda \mu\)-calculus
- Proof nets and explicit substitutions
- Proof nets and the call-by-value \(\lambda\)-calculus
- Resource operators for \(\lambda\)-calculus
- Reversible, irreversible and optimal \(\lambda\)-machines
- Rewriting Techniques and Applications
- The Prismoid of Resources
- The call-by-value λ-calculus: a semantic investigation
- The differential \(\lambda \mu\)-calculus
- The structural \(\lambda \)-calculus
- \(\rightthreetimes\)
Cited in
(19)- scientific article; zbMATH DE number 177801 (Why is no real title available?)
- scientific article; zbMATH DE number 7526055 (Why is no real title available?)
- On reduction and normalization in the computational core
- A new graphical calculus of proofs
- scientific article; zbMATH DE number 7456059 (Why is no real title available?)
- scientific article; zbMATH DE number 7356671 (Why is no real title available?)
- Strong call-by-value and multi types
- scientific article; zbMATH DE number 2134911 (Why is no real title available?)
- A Fresh Look at the λ-Calculus
- Jumping Boxes
- Open call-by-value
- The bang calculus and the two Girard's translations
- Proof nets and the call-by-value \(\lambda\)-calculus
- A formal equational theory for call-by-push-value
- Quantitative global memory
- Call-by-Value -calculus and LJQ
- Light genericity
- Proof nets and the linear substitution calculus
- Labelled \(\lambda\)-calculi with explicit copy and erase
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)
