Compositional termination checking with sized types

Iowa Type Theory Commute
30/03/2020 18 min Temporada 1 Episodio 62
Compositional termination checking with sized types

Listen "Compositional termination checking with sized types"

Descargar episodio

Episode Synopsis

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.
© 2003-2025 ZARZA | AHEAD OF OUR TIME
privacy policy
In God we trust In God we trust
PreSales Questions? Click Here
or call our toll-free line at +1-888-5002068 Miami, Florida, USA