Podcasts Technology Iowa Type Theory Commute Compositional termination checking with sized types

Compositional termination checking with sized types

Published: March 30, 2020, 7 p.m.

b'

Discussion of a compositional method of termination checking using so-called sized types.\\xa0 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.\\xa0 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.\\xa0 A readable and interesting tutorial on the subject is here.

'