Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-a...
summary
Extends a temporal type-and-effect system to handle delimited continuations (shift0/reset0) by tracking how continuations change the observable trace — the key idea is answer-effect modification. Supports dependently typed continuations so continuation types and traces can depend on values, and proves soundness: finite traces via type safety and infinite traces via a logical relation. Ships a prototype constraint generator for verification conditions but the constraint solver is still unimplemented; used on resource, exception, and backtracking examples.
AI-written summary · about
chapters (14)
- 0:00Start
- 1:01Example: resource usage
- 5:48Contribution
- 7:22Outline
- 7:42Brief introduction to shift0/reste0
- 9:38Example: exception
- 11:16Resource usage with exception
- 12:29Example: backtracking
- 14:30Resource usage with backtracking
- 16:06Challenge
- 17:31Similarity problem in reasoning about values
- 20:03Typing event raising
- 21:11Example: resuming continuations multiple times
- 21:45Related work