Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
From MaRDI portal
Publication:6137846
DOI10.46298/lmcs-19(4:23)2023arXiv2205.15203OpenAlexW4389732286MaRDI QIDQ6137846
Publication date: 16 January 2024
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2205.15203
Cites Work
- Unnamed Item
- Unnamed Item
- 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
- Differential interaction nets
- 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
- On the \(\pi\)-calculus and 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
- (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
- 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
- (Optimal) duplication is not elementary recursive
- A nonstandard standardization theorem
- A Semantical and Operational Account of Call-by-Value Solvability
- Term Rewriting and Applications
- A Local Criterion for Polynomial-Time Stratified Computations
- A syntax for linear logic
- Theoretical Computer Science
- Useful Open Call-By-Need
