| Generalised Simultaneous Inductive-Recursive De nitions and their Application to Programming in Type Theory (2007) | |||||||||||||||
Abstract | |||||||||||||||
| Abstract. In this work we present a generalisation of Dybjer's schema for simultaneous inductive-recursive denitions for the cases where we have several mutually recursive predicates dened simultaneously with several functions which, in turn, are dened by recursion on those predicates. As an application, we can use the methodology developed by Bove and Capretta for formalising general recursive algorithms to de-ne nested and mutually recursive algorithms in type theories extended with the generalised schema we present in this work. Hence, the resulting de nitions are such that the computational and logical parts are clearly separated. Moreover, the type-theoretic version of the algorithms is given by its purely functional content, similarly to the corresponding program in a functional programming language. 1 | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||