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.

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