Temporal Resource Typing: Enriching Substructural Typing for Liveness Reasoning
This program is tentative and subject to change.
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.
This program is tentative and subject to change.
Tue 14 OctDisplayed time zone: Perth change
16:00 - 17:40 | |||
16:00 30mTalk | Temporal Resource Typing: Enriching Substructural Typing for Liveness Reasoning IWACO | ||
16:30 30mTalk | Type Universes as Kripke Worlds: Memory Management Edition IWACO Paulette Koronkevich University of British Columbia | ||
17:00 30mTalk | TBD IWACO Mae Milano Princeton University |