Graded modalities have been proposed in recent work on programming languages as a general framework for refining type systems with intensional properties. In particular, continuous endomaps of the discrete time scale, or time warps, can be used to quantify the growth of information in the course of program execution. Time warps form a complete residuated lattice, with the residuals playing an important role in potential programming applications. In this paper, we study the algebraic structure of time warps, and prove that their equational theory is decidable, a necessary condition for their use in real-world compilers. We also describe how our universal-algebraic proof technique lends itself to a constraint-based implementation, establishing a new link between universal algebra and verification technology.

翻译：最近关于编程语言的工作提出了分级模式,作为精细具有加固特性的类型系统的一般框架,特别是可以使用离散时间尺度或时间扭曲的连续内径来量化程序执行过程中信息的增长。时间扭曲形成一个完全的再生的拉链,剩余部分在潜在的编程应用中发挥重要作用。我们在本文件中研究时间扭曲的代数结构,并证明它们的等式理论是可变的,是它们在现实世界汇编者中使用的必要条件。我们还描述了我们的通用代数校验技术如何有助于基于限制的执行,在通用代数与核查技术之间建立新的联系。