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 ...

• Type: Conference
• Year: 2008
• Where: CIE
• Authors: Ralph Matthes
• Keywords: Applied Computing, CIE 2008, Induction Principle, Nested Datatypes, Type Theory