Quantitative global memory
From MaRDI portal
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
- A new type assignment for λ-terms
- A Semantical and Operational Account of Call-by-Value Solvability
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- Call-By-Value, Again!
- Collapsing non-idempotent intersection types
- Execution time of λ-terms via denotational semantics and intersection types
- scientific article; zbMATH DE number 4179333 (Why is no real title available?)
- scientific article; zbMATH DE number 7559871 (Why is no real title available?)
- 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
- Towards a semantic measure of the execution time in call-by-value lambda-calculus
- Types of fireballs
Cited in
(3)
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)
