A semantic account of strong normalization in linear logic
DOI10.1016/J.IC.2015.12.010zbMath1353.03077arXiv1304.6762OpenAlexW1630373979MaRDI QIDQ276260
Daniel de Carvalho, Lorenzo Tortora de Falco
Publication date: 3 May 2016
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1304.6762
computational complexitycut eliminationlinear logicdenotational semanticsproof netsstrong normalization
Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Categorical semantics of formal languages (18C50) Proof-theoretic aspects of linear logic and other substructural logics (03F52)
Related Items (6)
Cites Work
- Unnamed Item
- The relational model is injective for multiplicative exponential linear logic (without weakenings)
- A semantic measure of the execution time in linear logic
- Linear logic
- Differential interaction nets
- Light affine lambda calculus and polynomial time strong normalization
- Uniformity and the Taylor expansion of ordinary lambda-terms
- Strong normalization property for second order linear logic
- An extension of basic functionality theory for \(\lambda\)-calculus
- Non-idempotent intersection types and strong normalisation
- Filter models: non-idempotent intersection types, orthogonality and polymorphism
- Linear Logic and Strong Normalization
- Complexity of Strongly Normalising λ-Terms via Non-idempotent Intersection Types
- The Inhabitation Problem for Non-idempotent Intersection Types
- Proving termination with multiset orderings
- Execution time of λ-terms via denotational semantics and intersection types
- The Relational Model Is Injective for Multiplicative Exponential Linear Logic
- Logical Approaches to Computational Barriers
This page was built for publication: A semantic account of strong normalization in linear logic
