Quantitative Global Memory
Programming Languages
2023-06-19 v5 Logic in Computer Science
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.
Cite
@article{arxiv.2303.08940,
title = {Quantitative Global Memory},
author = {Sandra Alves and Delia Kesner and Miguel Ramos},
journal= {arXiv preprint arXiv:2303.08940},
year = {2023}
}
Comments
WoLLIC 2023, full version (including proofs)