当程序必须看油漆干燥时
摘要：资源的安全使用，我们探索了类型系统和程序抽象。具体来说，我们研究了如何使用类型来模块化地指定和检查程序何时允许使用资源，例如，在生产线上编程机器人臂部时，关键是在组装之前给喷涂部件足够的时间干燥。我们采用一种时间分级的Fitch风格模态类型系统来捕捉这种时间资源，开发了一个相应的模态类型、有副作用的核心演算，并为其提供了一个具体的前层模型来说明分级单调的底层语义。我们的演算还包括有关时间的分级代数效果和效果处理程序。前者采用新颖的时间处理方式，其中操作的规范包括它们的执行时间，它们的延续知道在开始执行之前已经过了一段额外的时间，使得可以安全地访问更多的时间资源，在这些延续中，效果处理程序必须遵守这种时间纪律。
作者：Danel Ahman
论文ID：2210.07738
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-04-26