Quantitative global memory
From MaRDI portal
Publication:6199577
DOI10.1007/978-3-031-39784-4_4arXiv2303.08940MaRDI QIDQ6199577FDOQ6199577
Authors: Sandra Alves, Delia Kesner, Miguel Ramos 
Publication date: 28 February 2024
Published in: Logic, Language, Information, and Computation (Search for Journal in Brave)
Abstract: We show that recent approaches of static analysis based on quantitative typing systems can be extended to programming languages with global state. More precisely, we define a call-by-value language equipped with operations to access a global memory, together with a semantic model based on a (tight) multi-type system that captures exact measures of time and space related to evaluation of programs. We show that the type system is quantitatively sound and complete with respect to the original operational semantics of the language.
Full work available at URL: https://arxiv.org/abs/2303.08940
Cites Work
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- Linear logic
- Title not available (Why is that?)
- Execution time of λ-terms via denotational semantics and intersection types
- A new type assignment for λ-terms
- Intersection types and computational effects
- A Semantical and Operational Account of Call-by-Value Solvability
- Proof nets and the call-by-value \(\lambda\)-calculus
- Intersection, Universally Quantified, and Reference Types
- The bang calculus revisited
- Non-idempotent intersection types for the lambda-calculus
- Collapsing non-idempotent intersection types
- Title not available (Why is that?)
- Tight typings and split bounds, fully developed
- Types of fireballs
- Call-By-Value, Again!
- Syntax and semantics of quantitative type theory
- New semantical insights into call-by-value \(\lambda\)-calculus
- Title not available (Why is that?)
- On reduction and normalization in the computational core
This page was built for publication: Quantitative global memory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6199577)
