Execution time of λ-terms via denotational semantics and intersection types

DOI10.1017/S0960129516000396zbMath1475.03073arXiv0905.4251OpenAlexW2964032597MaRDI QIDQ4577984

Daniel de Carvalho

Publication date: 7 August 2018

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

denotational semanticslambda calculusintersection types

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items

A semantic account of strong normalization in linear logic ⋮ A type assignment for \(\lambda\)-calculus complete both for FPTIME and strong normalization ⋮ Taylor expansion, finiteness and strategies ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Transport of finiteness structures and applications ⋮ Non-Deterministic Functions as Non-Deterministic Processes (Extended Version) ⋮ From semantics to types: the case of the imperative \(\lambda\)-calculus ⋮ Quantitative global memory ⋮ Non-idempotent intersection types in logical form ⋮ The relational model is injective for multiplicative exponential linear logic (without weakenings) ⋮ Tight typings and split bounds, fully developed ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A semantic measure of the execution time in linear logic ⋮ Unnamed Item ⋮ The bang calculus revisited ⋮ Unnamed Item ⋮ Unnamed Item ⋮ The bang calculus revisited ⋮ A Fresh Look at the λ-Calculus ⋮ Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A semantic measure of the execution time in linear logic
• Linear logic
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Differential interaction nets
• The system \({\mathcal F}\) of variable types, fifteen years later
• Principal type scheme and unification for intersection type discipline
• Head linear reduction and pure proof net extraction
• A call-by-name lambda-calculus machine
• Compositional characterisations of \(\lambda\)-terms using intersection types
• Not Enough Points Is Enough
• A linearization of the Lambda-calculus and consequences
• A semantics for lambda calculi with resources
• The lambda calculus is algebraic
• Types, potency, and idempotency
• Logical Approaches to Computational Barriers
• On phase semantics and denotational semantics: The exponentials