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.

翻译：---- 我们展示了最近的基于定量类型系统的静态分析方法可以扩展到具有全局状态的编程语言。更确切地说，我们定义了一个按值调用的语言，配备了访问全局存储器的操作，以及基于（严格的）多类型系统的语义模型，捕获与程序评估相关的时间和空间的精确度量。我们展示了类型系统相对于原始操作语义是定量上完备和可靠的。