Quantitative global memory
From MaRDI portal
Publication:6199577
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.
Cites work
- scientific article; zbMATH DE number 4179333 (Why is no real title available?)
- scientific article; zbMATH DE number 7526055 (Why is no real title available?)
- scientific article; zbMATH DE number 7559871 (Why is no real title available?)
- A Semantical and Operational Account of Call-by-Value Solvability
- A new type assignment for λ-terms
- Call-By-Value, Again!
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- Collapsing non-idempotent intersection types
- Execution time of λ-terms via denotational semantics and intersection types
- Intersection types and computational effects
- Intersection, Universally Quantified, and Reference Types
- Linear logic
- New semantical insights into call-by-value \(\lambda\)-calculus
- Non-idempotent intersection types for the lambda-calculus
- On reduction and normalization in the computational core
- Proof nets and the call-by-value \(\lambda\)-calculus
- Syntax and semantics of quantitative type theory
- The bang calculus revisited
- Tight typings and split bounds, fully developed
- Types of fireballs
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)
