Exponentials as substitutions and the cost of cut elimination in linear logic
From MaRDI portal
Publication:6649484
DOI10.1145/3531130.3532445MaRDI QIDQ6649484
Publication date: 6 December 2024
Cut-elimination and normal-form theorems (03F05) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Combinatory logic and lambda calculus (03B40)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Linear logical relations and observational equivalences for session-based concurrency
- A semantic measure of the execution time in linear logic
- Linear logic
- Computational interpretations of linear logic
- Resource operators for \(\lambda\)-calculus
- Strong normalization property for second order linear logic
- A list-oriented extension of the lambda-calculus satisfying the Church-Rosser theorem
- Bounded linear logic: A modular approach to polynomial-time computability
- Light linear logic
- Head linear reduction and pure proof net extraction
- Lambda calculus and intuitionistic linear logic
- Linear logic and elementary time
- Call-by-name, call-by-value, call-by-need and the linear lambda calculus
- Proof nets and the linear substitution calculus
- Soft linear logic and polynomial time
- An abstract machine for strong call by value
- (Leftmost-Outermost) Beta Reduction is Invariant, Indeed
- Distilling abstract machines
- A theory of effects and resources: adjunction models and polarised calculi
- A Calculus for Interaction Nets Based on the Linear Chemical Abstract Machine
- Local Bigraphs and Confluence: Two Conjectures
- Call-by-Value Solvability, Revisited
- On Constructor Rewrite Systems and the Lambda Calculus
- Labelled calculi of resources
- Bounding linear head reduction and visible interaction through skeletons
- The duality of computation
- Linear Logic and Strong Normalization
- A Theory of Explicit Substitutions with Safe and Full Composition
- A Strong Distillery
- Union of Reducibility Candidates for Orthogonal Constructor Rewriting
- A Terminating and Confluent Linear Lambda Calculus
- On the Relations between the Syntactic Theories of λμ-Calculi
- Session Types as Intuitionistic Linear Propositions
- The Structural λ-Calculus
- The Theory of Calculi with Explicit Substitutions Revisited
- Confluence of Pure Differential Nets with Promotion
- Linear explicit substitutions
- A new correctness criterion for MLL proof nets
- Strong normalisation for the linear term calculus
- Explicit substitutions
- Propositions as sessions
- A nonstandard standardization theorem
- A Semantical and Operational Account of Call-by-Value Solvability
- Term Rewriting and Applications
- A syntax for linear logic
- Theoretical Computer Science
This page was built for publication: Exponentials as substitutions and the cost of cut elimination in linear logic
