Types of fireballs

DOI10.1007/978-3-030-02768-1_3MaRDI QIDQ6166135zbMATH OpenOpenAlexFDO

Authors Beniamino Accattoli, Giulio Guerrieri

Publication date 2 August 2023

Published in Programming Languages and Systems (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Abstract: The good properties of Plotkin's call-by-value lambda-calculus crucially rely on the restriction to weak evaluation and closed terms. Open call-by-value is the more general setting where evaluation is weak but terms may be open. Such an extension is delicate, and the literature contains a number of proposals. Recently, Accattoli and Guerrieri provided detailed operational and implementative studies of these proposals, showing that they are equivalent from the point of view of termination, and also at the level of time cost models. This paper explores the denotational semantics of open call-by-value, adapting de Carvalho's analysis of call-by-name via multi types (aka non-idempotent intersection types). Our type system characterises normalisation and thus provides an adequate relational semantics. Moreover, type derivations carry quantitative information about the cost of evaluation: their size bounds the number of evaluation steps and the size of the normal form, and we also characterise derivations giving exact bounds. The study crucially relies on a new, refined presentation of the fireball calculus, the simplest proposal for open call-by-value, that is more apt to denotational investigations.

Recommendations

• Open call-by-value
• On the Relative Usefulness of Fireballs
• Implementing open call-by-value
• scientific article; zbMATH DE number 6825409
• New semantical insights into call-by-value \(\lambda\)-calculus

Cited in

(15)

• The bang calculus revisited
• Open call-by-value
• On the Relative Usefulness of Fireballs
• Towards a semantic measure of the execution time in call-by-value lambda-calculus
• A Fresh Look at the λ-Calculus
• Tight typings and split bounds, fully developed
• scientific article; zbMATH DE number 7756108 (Why is no real title available?)
• The bang calculus revisited
• Quantitative weak linearisation
• Quantitative global memory
• Strong call-by-value and multi types
• Light genericity
• Semantic bounds and multi types, revisited
• A quantitative approach to global state composition
• Hybrid intersection types for PCF

This page was built for publication: Types of fireballs

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