A semantic measure of the execution time in linear logic

DOI10.1016/J.TCS.2010.12.017zbMath1222.03070OpenAlexW2081694512MaRDI QIDQ534698

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 complexitycut eliminationlinear logicdenotational 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)

Related Items (19)

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

Cites Work

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

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