Resources are stateful objects that must be used according to specific protocols during program execution. These protocols can be formally expressed as temporal properties over event traces that represent resource usage, incorporating both safety and liveness. Existing approaches to resource usage analysis focus on the safety aspects of resource usage while ignoring liveness requirements.

To address this gap, we propose temporal resource typing to support liveness reasoning of resource usage. A main novelty is that it enriches the types of resources with a resettable timer mechanism that provides a progressivity guarantee for infinite resource usage in divergent program executions. We demonstrate the usefulness of our type system by examples and prove soundness.