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.

Abstract Intermittent computing is gaining traction in application domains such as Energy Harvesting Devices (EHDs) that experience arbitrary power failures during program execution. To make progress, programs require system support to checkpoint state and re-execute after power failure by restoring the last saved state. This re-execution should becorrect, 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. We define a Crash type system for a core calculus. We prove the correctness of intermittent systems by defining a novel logical relation for Crash types.