Start / Iowa Type Theory Commute / Compositional termination checking with sized types

Compositional termination checking with sized types

19 min • 30 mars 2020

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.