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.

翻译：我们证明了基于定量类型系统的静态分析方法可以扩展到具有全局状态的编程语言。具体而言，我们定义了一种按值调用的语言，该语言配备了访问全局内存的操作，并基于（严谨的）多类型系统构建了一个语义模型，该模型能够捕获程序求值过程中时间和空间的精确度量。我们证明了该类型系统在语言原始操作语义下具有定量可靠性和完备性。