MiniAgda: Integrating Sized and Dependent Types

Andreas Abel

Sized types are a modular and theoretically well-understood tool for checking termination of recursive and productivity of corecursive definitions. The essential idea is to track s…