Recursion on Nested Datatypes in Dependent Type Theory

13 years 7 months ago
Recursion on Nested Datatypes in Dependent Type Theory
Nested datatypes are families of datatypes that are indexed over all types and where the datatype constructors relate different members of the family. This may be used to represent variable binding or to maintain certain invariants through typing. In dependent type theory, a major concern is the termination of all expressible programs, so that types that depend on object terms can still be type-checked mechanically. Therefore, we study iteration and recursion schemes that have this termination guarantee throughout. This is not based on syntactic criteria (recursive calls with "smaller" arguments) but just on types ("type-based termination"). An important concern are reasoning principles that are compatible with the ambient type theory, in our case induction principles. ous work, the author has proposed an abstract description of nested datatypes together with a mapping operation (like map for lists) and an iterator on the term side and an induction principle on the ...
Ralph Matthes
Added 12 Oct 2010
Updated 12 Oct 2010
Type Conference
Year 2008
Where CIE
Authors Ralph Matthes
Comments (0)