EPISODE · Mar 30, 2020 · 18 MIN
Compositional termination checking with sized types
from Iowa Type Theory Commute · host Aaron Stump
Discussion of a compositional method of termination checking using so-called sized types. Datatypes are indexed by sizes, and recursive calls can only be made on data of strictly smaller size than the data as input to the recursion. Since the method is type-based, it is compositional: we can break out helper functions from a recursive function and not upset the termination checker. A readable and interesting tutorial on the subject is here.
What this episode covers
Discussion of a compositional method of termination checking using so-called sized types. Datatypes are indexed by sizes, and recursive calls can only be made on data of strictly smaller size than the data as input to the recursion. Since the method is type-based, it is compositional: we can break out helper functions from a recursive function and not upset the termination checker. A readable and interesting tutorial on the subject is here.
NOW PLAYING
Compositional termination checking with sized types
No transcript for this episode yet
Similar Episodes
Mar 4, 2026 ·7m
Feb 22, 2026 ·9m
Feb 8, 2026 ·11m
Feb 2, 2026 ·12m
Jan 30, 2026 ·31m
Jan 29, 2026 ·39m