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

DOI10.1017/S0960129516000396MaRDI QIDQ4577984zbMATH OpenOpenAlexFDO

Authors 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)

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.

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 -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

Cites work

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

Cited in

(25)

• scientific article; zbMATH DE number 7559283 (Why is no real title available?)
• scientific article; zbMATH DE number 7089070 (Why is no real title available?)
• A semantic account of strong normalization in linear logic
• A type assignment for -calculus complete both for FPTIME and strong normalization
• Tight typings and split bounds, fully developed
• scientific article; zbMATH DE number 7526055 (Why is no real title available?)
• scientific article; zbMATH DE number 7577566 (Why is no real title available?)
• The relational model is injective for multiplicative exponential linear logic (without weakenings)
• A semantic measure of the execution time in linear logic
• scientific article; zbMATH DE number 7003195 (Why is no real title available?)
• 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\)
• scientific article; zbMATH DE number 7155170 (Why is no real title available?)
• Transport of finiteness structures and applications
• From semantics to types: the case of the imperative \(\lambda\)-calculus
• scientific article; zbMATH DE number 7471682 (Why is no real title available?)
• scientific article; zbMATH DE number 7756108 (Why is no real title available?)
• 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)