Towards a semantic measure of the execution time in call-by-value lambda-calculus

MaRDI QIDQ5076060zbMATH OpenFDO

Authors Giulio Guerrieri

Publication date 12 May 2022

Full work available at URL https://arxiv.org/abs/1904.10800, http://eptcs.web.cse.unsw.edu.au/paper.cgi?ITRS2018.5

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Recommendations

• Execution time of λ-terms via denotational semantics and intersection types
• A semantic measure of the execution time in linear logic
• Call-by-value, elementary time and intersection types
• Types of fireballs

Cites work

• A compiled implementation of strong reduction
• A linearization of the Lambda-calculus and consequences
• A new type assignment for λ-terms
• A relational semantics for parallelism and non-determinism in a functional setting
• A resource aware computational interpretation for Herbelin's syntax
• A semantic account of strong normalization in linear logic
• A semantic measure of the execution time in linear logic
• A Semantical and Operational Account of Call-by-Value Solvability
• A type assignment for -calculus complete both for FPTIME and strong normalization
• An equivalence between lambda- terms
• An extension of basic functionality theory for -calculus
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Call-by-value non-determinism in a linear logic type discipline
• Call-by-value solvability, revisited
• Collapsing non-idempotent intersection types
• Essential and relational models
• Execution time of λ-terms via denotational semantics and intersection types
• Head reduction and normalization in a call-by-value lambda-calculus
• scientific article; zbMATH DE number 3657760 (Why is no real title available?)
• scientific article; zbMATH DE number 482822 (Why is no real title available?)
• scientific article; zbMATH DE number 2044494 (Why is no real title available?)
• scientific article; zbMATH DE number 1479634 (Why is no real title available?)
• scientific article; zbMATH DE number 6825409 (Why is no real title available?)
• scientific article; zbMATH DE number 7204443 (Why is no real title available?)
• scientific article; zbMATH DE number 236855 (Why is no real title available?)
• Linear logic
• Non-idempotent intersection types and strong normalisation
• Non-idempotent intersection types for the lambda-calculus
• Normal functors, power series and -calculus
• On phase semantics and denotational semantics: The exponentials
• On the Relative Usefulness of Fireballs
• Open call-by-value
• Proof nets and the call-by-value \(\lambda\)-calculus
• Standardization of a Call-By-Value Lambda-Calculus
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The parametric lambda calculus. A metamodel for computation.
• Tight typings and split bounds, fully developed
• Types by need
• Types of fireballs
• Types, potency, and idempotency: why nonlinearity and amnesia make a type system work

Cited in

(8)

• The bang calculus revisited
• scientific article; zbMATH DE number 1497774 (Why is no real title available?)
• Execution time of λ-terms via denotational semantics and intersection types
• On reduction and normalization in the computational core
• The bang calculus revisited
• Quantitative global memory
• Strong call-by-value and multi types
• A quantitative approach to global state composition

This page was built for publication: Towards a semantic measure of the execution time in call-by-value lambda-calculus

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