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.

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