A semantic measure of the execution time in linear logic

DOI10.1016/J.TCS.2010.12.017zbMATH Open1222.03070OpenAlexW2081694512MaRDI QIDQ534698FDOQ534698

Michele Pagani, Daniel de Carvalho, Lorenzo Tortora de Falco

Publication date: 10 May 2011

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/inria-00206099/file/RR-6441.pdf

zbMATH Keywords

computational complexitylinear logiccut eliminationdenotational semanticscut-free normal form of a MELL net

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Cut-elimination and normal-form theorems (03F05) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Cites Work

• Linear logic
• Strong normalization property for second order linear logic
• Light linear logic
• Execution time of λ-terms via denotational semantics and intersection types
• Title not available (Why is that?)
• Logical Approaches to Computational Barriers
• Uniformity and the Taylor expansion of ordinary lambda-terms
• The structure of multiplicatives
• Obsessional experiments for linear logic proof-nets
• Proofs, denotational semantics and observational equivalences in Multiplicative Linear Logic
• Stratified coherence spaces: A denotational semantics for light linear logic
• Title not available (Why is that?)
• Intersection types for light affine lambda calculus
• Partial Types and Intervals
• Quantitative Game Semantics for Linear Logic
• Logical Approaches to Computational Barriers

Cited In (20)

• Execution time of λ-terms via denotational semantics and intersection types
• Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
• Polynomial time in untyped elementary linear logic
• Tight typings and split bounds, fully developed
• Visible acyclic differential nets. I: Semantics
• LINEAR TIME IN HYPERSEQUENT FRAMEWORK
• Exact bounds for acyclic higher-order recursion schemes
• Title not available (Why is that?)
• A semantic account of strong normalization in linear logic
• The relational model is injective for multiplicative exponential linear logic (without weakenings)
• Title not available (Why is that?)
• Strong call-by-value and multi types
• Factorization in call-by-name and call-by-value calculi via linear logic
• A Fresh Look at the λ-Calculus
• Title not available (Why is that?)
• The bang calculus revisited
• The bang calculus revisited
• Exponentials as substitutions and the cost of cut elimination in linear logic
• Factorization and normalization, essentially
• Title not available (Why is that?)

   Recommendations

• A semantic account of strong normalization in linear logic 👍 👎
• Interaction nets for linear logic 👍 👎
• Execution time of λ-terms via denotational semantics and intersection types 👍 👎
• Linear logic by levels and bounded time complexity 👍 👎
• Quantitative Game Semantics for Linear Logic 👍 👎

This page was built for publication: A semantic measure of the execution time in linear logic

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