一句话：提出崩溃类型系统与模态逻辑基础，用于建模并证明间歇计算中检查点与重执行的正确性。
能量收集设备等间歇执行环境随时可能断电，系统需在运行时保存检查点并在崩溃后恢复、重执行，且重执行必须等价于持续供电下的执行。本文研究间歇计算的逻辑基础，将检查点、崩溃、恢复和重执行建模为对“崩溃类型”的计算，并借鉴伴随逻辑引入两个伴随模态算子，分别刻画部分（重）执行中的持久与瞬态内存值，以及检查点和恢复引发的状态转换。该形式化可容纳多种检查点策略。作者为核心演算定义崩溃类型系统，并设计一种面向崩溃类型的新型逻辑关系，以证明间歇系统的正确性。
Programs are executed intermittently on devices that experience arbitrary power failures such as Energy Harvesting Devices (EHDs). To ensure progress, intermittent systems need runtime support to checkpoint state and re-execute after power failure by restoring the last saved state. Such re-execution should be correct , i.e., simulated by a continuously-powered execution. We study the logical underpinning of intermittent computing and model checkpoint, crash, restore, and re-execution operations as computation on crash types. We draw inspiration from adjoint logic and define crash types by introducing two adjoint modality operators to model persistent and transient memory values of partial (re-)executions and the transitions between them caused by checkpoints and restoration. Our formalism is general enough to accommodate a variety of checkpointing policies. We define a crash type system for a core calculus. To prove the correctness of intermittent systems, we define a novel logical relation for crash types.