ICFP/SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore

This program is tentative and subject to change.

Tue 14 Oct 2025 16:00 - 16:30 at Peony NE - Type systems

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 Oct

Displayed time zone: Perth change

16:00 - 17:40
Type systemsIWACO at Peony NE
16:00
30m
Talk
Temporal Resource Typing: Enriching Substructural Typing for Liveness Reasoning
IWACO
Yiyuan Cao Peking University, Taro Sekiyama National Institute of Informatics
16:30
30m
Talk
Type Universes as Kripke Worlds: Memory Management Edition
IWACO
Paulette Koronkevich University of British Columbia
17:00
30m
Talk
TBD
IWACO
Mae Milano Princeton University