A semantic account of strong normalization in linear logic

DOI10.1016/J.IC.2015.12.010MaRDI QIDQ276260zbMATH OpenOpenAlexFDO

Authors 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

zbMATH Keywords

computational complexitylinear logiccut eliminationdenotational semanticsproof netsstrong normalization

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Logic in computer science (03B70) Structure of proofs (03F07) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Categorical semantics of formal languages (18C50)

Abstract: We prove that given two cut free nets of linear logic, by means of their relational interpretations one can: 1) first determine whether or not the net obtained by cutting the two nets is strongly normalizable 2) then (in case it is strongly normalizable) compute the maximal length of the reduction sequences starting from that net.

Recommendations

• Linear Logic and Strong Normalization
• Publication:4896506
• A semantic measure of the execution time in linear logic
• Strong normalization property for second order linear logic
• The conservation theorem for differential nets

Cites work

• scientific article; zbMATH DE number 786499 (Why is no real title available?)
• A semantic measure of the execution time in linear logic
• An extension of basic functionality theory for -calculus
• Complexity of Strongly Normalising λ-Terms via Non-idempotent Intersection Types
• Differential interaction nets
• Execution time of λ-terms via denotational semantics and intersection types
• Filter models: non-idempotent intersection types, orthogonality and polymorphism
• Light affine lambda calculus and polynomial time strong normalization
• Linear Logic and Strong Normalization
• Linear logic
• Logical Approaches to Computational Barriers
• Non-idempotent intersection types and strong normalisation
• Proving termination with multiset orderings
• Strong normalization property for second order linear logic
• The Inhabitation Problem for Non-idempotent Intersection Types
• The relational model is injective for multiplicative exponential linear logic
• The relational model is injective for multiplicative exponential linear logic (without weakenings)
• Uniformity and the Taylor expansion of ordinary lambda-terms

Cited in

(17)

• scientific article; zbMATH DE number 1405619 (Why is no real title available?)
• The conservation theorem for differential nets
• Tight typings and split bounds, fully developed
• scientific article; zbMATH DE number 7526055 (Why is no real title available?)
• The relational model is injective for multiplicative exponential linear logic (without weakenings)
• A semantic measure of the execution time in linear logic
• scientific article; zbMATH DE number 7003195 (Why is no real title available?)
• Strong normalization property for second order linear logic
• A By-Level Analysis of Multiplicative Exponential Linear Logic
• On proof normalization in linear logic
• The bang calculus revisited
• Context semantics, linear logic, and computational complexity
• The bang calculus revisited
• The Cut-Elimination Theorem for Differential Nets with Promotion
• Linear Logic and Strong Normalization
• scientific article; zbMATH DE number 7756108 (Why is no real title available?)
• From propositional to linear logic: An introduction. Decoration, simulation, normalization

This page was built for publication: A semantic account of strong normalization in linear logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q276260)