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 semanticsintersection typeslambda calculus

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

• 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
• 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?)
• 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

(43)

• The bang calculus revisited
• Taylor expansion, finiteness and strategies
• Non-idempotent intersection types in logical form
• A semantic account of strong normalization in linear logic
• A type assignment for -calculus complete both for FPTIME and strong normalization
• A non-uniform finitary relational semantics of system T
• The relational model is injective for multiplicative exponential linear logic (without weakenings)
• Transport of finiteness structures and applications
• scientific article; zbMATH DE number 7003195 (Why is no real title available?)
• scientific article; zbMATH DE number 7471682 (Why is no real title available?)
• Towards a semantic measure of the execution time in call-by-value lambda-calculus
• A Fresh Look at the λ-Calculus
• Differentials and distances in probabilistic coherence spaces
• Differentials and distances in probabilistic coherence spaces
• Semantic evaluation; intersection types and complexity of simply typed lambda calculus
• Tight typings and split bounds, fully developed
• Non-idempotent types for classical calculi in natural deduction style
• scientific article; zbMATH DE number 7089070 (Why is no real title available?)
• A semantic measure of the execution time in linear logic
• scientific article; zbMATH DE number 7756108 (Why is no real title available?)
• From semantics to types: the case of the imperative \(\lambda\)-calculus
• The bang calculus revisited
• Quantitative global memory
• Strong call-by-value and multi types
• From semantics to types: the case of the imperative \(\lambda\)-calculus
• Categorifying non-idempotent intersection types
• A deep quantitative type system
• Solvability in a probabilistic setting (invited talk)
• Tropical mathematics and the lambda-calculus I: metric and differential analysis of effectful programs
• Semantic bounds and multi types, revisited
• From thin concurrent games to generalized species of structures (extended version)
• Böhm and Taylor for all!
• Mirroring call-by-need, or values acting silly
• Mechanized subject expansion in uniform intersection types for perpetual reductions
• Meaningfulness and genericity in a subsuming framework (invited talk)
• (Definitely not) boring interaction abstract machines
• A quantitative approach to global state composition
• An analysis of symmetry in quantitative semantics
• The relational machine calculus
• Title not available (Why is no real title available?)
• Title not available (Why is no real title available?)
• Title not available (Why is no real title available?)
• Title not available (Why is no real title available?)

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)