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

geometry of interactionimplicit computational complexitylinear logic

Mathematics Subject Classification ID

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

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)

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

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)