A semantic measure of the execution time in linear logic
DOI10.1016/J.TCS.2010.12.017zbMATH Open1222.03070OpenAlexW2081694512MaRDI QIDQ534698FDOQ534698
Authors: Daniel de Carvalho, Michele Pagani, 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
Recommendations
computational complexitylinear logiccut eliminationdenotational semanticscut-free normal form of a MELL net
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?)
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)
