论文标题
当程序必须看油漆干燥时
When Programs Have to Watch Paint Dry
论文作者
论文摘要
我们探索类型系统和编程摘要，以安全地使用资源。特别是，我们研究了如何使用类型来模块化指定和检查何时允许程序使用其资源，例如，在对生产线上编程机器人臂进行编程时，至关重要的是，在组装之前，涂漆的零件有足够的时间来干燥。我们使用惠誉式模态类型系统的时间级变体捕获这种时间资源，开发相应的模态，有效的核心微积分，并为其配备由混凝土前eafeaf模型所说明的分级单位式示范语义。我们的演算还包括暂时意识的分级代数效应和效应处理程序。为前者提供了一种新颖的时间治疗，其中操作的规格包括其执行时间，并且他们的连续性知道，在开始执行之前，运营的额外时间已经过去了，这使得可以安全地访问其中的更多时间资源，以及效果处理人员必须尊重这种时间纪律。
We explore type systems and programming abstractions for the safe use of resources. In particular, we investigate how to use types to modularly specify and check when programs are allowed to use their resources, e.g., when programming a robot arm on a production line, it is crucial that painted parts are given enough time to dry before assembly. We capture such temporal resources using a time-graded variant of Fitch-style modal type systems, develop a corresponding modally typed, effectful core calculus, and equip it with a graded-monadic denotational semantics illustrated by a concrete presheaf model. Our calculus also includes temporally-aware graded algebraic effects and effect handlers. The former are given a novel temporal treatment, where operations' specifications include their execution times, and their continuations know that an operation's worth of additional time has passed before they start executing, making it possible to safely access further temporal resources in them, and where effect handlers have to respect this temporal discipline.
