Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
From MaRDI portal
Publication:6137846
DOI10.46298/LMCS-19(4:23)2023OpenAlexW4389732286MaRDI QIDQ6137846FDOQ6137846
Authors: Beniamino Accattoli 
Publication date: 16 January 2024
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Abstract: This paper introduces the exponential substitution calculus (ESC), a new presentation of cut elimination for IMELL, based on proof terms and building on the idea that exponentials can be seen as explicit substitutions. The idea in itself is not new, but here it is pushed to a new level, inspired by Accattoli and Kesner's linear substitution calculus (LSC). One of the key properties of the LSC is that it naturally models the sub-term property of abstract machines, that is the key ingredient for the study of reasonable time cost models for the -calculus. The new ESC is then used to design a cut elimination strategy with the sub-term property, providing the first polynomial cost model for cut elimination with unconstrained exponentials. For the ESC, we also prove untyped confluence and typed strong normalization, showing that it is an alternative to proof nets for an advanced study of cut elimination.
Full work available at URL: https://arxiv.org/abs/2205.15203
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- (Leftmost-outermost) beta reduction is invariant, indeed
- (Optimal) duplication is not elementary recursive
- A Local Criterion for Polynomial-Time Stratified Computations
- A Semantical and Operational Account of Call-by-Value Solvability
- A Terminating and Confluent Linear Lambda Calculus
- A Theory of Explicit Substitutions with Safe and Full Composition
- A calculus for interaction nets based on the linear chemical abstract machine
- A list-oriented extension of the lambda-calculus satisfying the Church-Rosser theorem
- A new correctness criterion for MLL proof nets
- A nonstandard standardization theorem
- A semantic measure of the execution time in linear logic
- A strong distillery
- A syntax for linear logic
- A theory of effects and resources: adjunction models and polarised calculi
- An abstract factorization theorem for explicit substitutions
- Bounded linear logic: A modular approach to polynomial-time computability
- Bounding linear head reduction and visible interaction through skeletons
- Call-by-name, call-by-value, call-by-need and the linear lambda calculus
- Call-by-value solvability, revisited
- Computational interpretations of linear logic
- Confluence of Pure Differential Nets with Promotion
- Differential interaction nets
- Distilling abstract machines
- Explicit substitutions
- Head linear reduction and pure proof net extraction
- Labelled calculi of resources
- Lambda calculus and intuitionistic linear logic
- Light linear logic
- Linear Logic and Strong Normalization
- Linear explicit substitutions
- Linear logic
- Linear logic and elementary time
- Linear logical relations and observational equivalences for session-based concurrency
- Local bigraphs and confluence: two conjectures (extended abstract)
- On constructor rewrite systems and the lambda calculus
- On the Relations between the Syntactic Theories of λμ-Calculi
- On the \(\pi\)-calculus and linear logic
- On the computational complexity of cut-elimination in linear logic.
- On the invariance of the unitary cost model for head reduction
- Proof nets and the linear substitution calculus
- Propositions as sessions
- Resource operators for \(\lambda\)-calculus
- Session types as intuitionistic linear propositions
- Soft linear logic and polynomial time
- Solvability = typability + inhabitation
- Strong normalisation for the linear term calculus
- Strong normalization property for second order linear logic
- Term Rewriting and Applications
- The Theory of Calculi with Explicit Substitutions Revisited
- The duality of computation
- The structural \(\lambda \)-calculus
- Useful Open Call-By-Need
This page was built for publication: Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6137846)
