Context semantics, linear logic, and computational complexity

DOI10.1145/1555746.1555749MaRDI QIDQ2946582zbMATH OpenOpenAlexWikidataFDO

Authors Ugo Dal Lago

Publication date 17 September 2015

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/cs/0510092

zbMATH Keywords

implicit computational complexitylinear logicgeometry of interaction

Mathematics Subject Classification ID

Complexity of proofs (03F20) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Complexity of computation (including implicit computational complexity) (03D15)

Abstract: We show that context semantics can be fruitfully applied to the quantitative analysis of proof normalization in linear logic. In particular, context semantics lets us define the weight of a proof-net as a measure of its inherent complexity: it is both an upper bound to normalization time (modulo a polynomial overhead, independently on the reduction strategy) and a lower bound to the number of steps to normal form (for certain reduction strategies). Weights are then exploited in proving strong soundness theorems for various subsystems of linear logic, namely elementary linear logic, soft linear logic and light linear logic.

Recommendations

• scientific article; zbMATH DE number 1948160
• On context semantics and interaction nets
• Quantitative Game Semantics for Linear Logic
• A semantic account of strong normalization in linear logic
• Linear logic and polynomial time

Cited in

(14)

• Towards a geometry of recursion
• Polynomial time in untyped elementary linear logic
• scientific article; zbMATH DE number 1954368 (Why is no real title available?)
• Context-Sensitive Languages, Rational Graphs and Determinism
• The computational complexity of ideal semantics
• Linear dependent types in a call-by-value scenario
• Implicit computation complexity in higher-order programming languages
• Characterizing polynomial and exponential complexity classes in elementary lambda-calculus
• Paths-based criteria and application to linear logic subsystems characterizing polynomial time
• On paths-based criteria for polynomial time complexity in proof-nets
• Is the Optimal Implementation Inefficient? Elementarily Not
• Quantitative Game Semantics for Linear Logic
• Geometry of resource interaction and Taylor-Ehrhard-Regnier expansion: \textit{a minimalist approach}
• Geometry of resource interaction -- \textit{a minimalist approach}

This page was built for publication: Context semantics, linear logic, and computational complexity

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