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

DOI10.1017/S0960129516000396zbMATH Open1475.03073arXiv0905.4251OpenAlexW2964032597MaRDI QIDQ4577984FDOQ4577984

Authors: Daniel de Carvalho 

Publication date: 7 August 2018

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

Abstract: The multiset based relational model of linear logic induces a semantics of the type free lambda-calculus, which corresponds to a non-idempotent intersection type system, System R. We prove that, in System R, the size of the type derivations and the size of the types are closely related to the execution time of lambda-terms in a particular environment machine, Krivine's machine.

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

Recommendations

• Semantic evaluation; intersection types and complexity of simply typed lambda calculus
• scientific article; zbMATH DE number 1759417
• Compositional characterisations of \(\lambda\)-terms using intersection types
• Intersection types for lambda-terms and combinators and their logics
• The complexity of type inference for higher-order typed lambda calculi
• Automatic binding time analysis for a typed \(\lambda\)-calculus
• Complexity of Strongly Normalising λ-Terms via Non-idempotent Intersection Types
• Towards a semantic measure of the execution time in call-by-value lambda-calculus
• Linearization of the lambda-calculus and its relation with intersection type systems
• A typed lambda calculus with intersection types

zbMATH Keywords

denotational semanticslambda calculusintersection types

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Cites Work

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

Cited In (25)

• Title not available (Why is that?)
• Title not available (Why is that?)
• Tight typings and split bounds, fully developed
• Title not available (Why is that?)
• Title not available (Why is that?)
• A semantic account of strong normalization in linear logic
• A type assignment for \(\lambda\)-calculus complete both for FPTIME and strong normalization
• The relational model is injective for multiplicative exponential linear logic (without weakenings)
• Title not available (Why is that?)
• A semantic measure of the execution time in linear logic
• Taylor expansion, finiteness and strategies
• Strong call-by-value and multi types
• A Fresh Look at the λ-Calculus
• Semantic evaluation; intersection types and complexity of simply typed lambda calculus
• The bang calculus revisited
• Quantitative global memory
• The bang calculus revisited
• From semantics to types: the case of the imperative \(\lambda\)-calculus
• A non-uniform finitary relational semantics of system \(T\)
• Title not available (Why is that?)
• Transport of finiteness structures and applications
• From semantics to types: the case of the imperative \(\lambda\)-calculus
• Title not available (Why is that?)
• Title not available (Why is that?)
• Non-idempotent intersection types in logical form

This page was built for publication: Execution time of λ-terms via denotational semantics and intersection types

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