### Skapa referens, olika format (klipp och klistra)

**Harvard**

Bove, A. och Capretta, V. (2001) *Nested General Recursion and Partiality in Type Theory*.

** BibTeX **

@conference{

Bove2001,

author={Bove, Ana and Capretta, Venanzio},

title={Nested General Recursion and Partiality in Type Theory},

booktitle={Theorem Proving in Higher Order Logics},

isbn={3-540-42525-X},

pages={121--135},

abstract={ We extend Bove's technique for formalising simple general recursive algorithms in constructive type theory to nested recursive algorithms. The method consists in defining an inductive domain predicate, that characterises the inputs on which the algorithm terminates. As a result, the type-theoretic version of the algorithm can be defined by structural recursion on the proof that the input values satisfy this predicate. This technique results in definitions in which the computational and logical parts are clearly separated; hence, the type-theoretic version of the algorithm is given by its purely functional content, similarly to the corresponding program in a functional programming language. In the case of nested recursion, the special predicate and the type-theoretic algorithm must be defined simultaneously, because they depend on each other. This kind of definitions is not allowed in ordinary type theory, but it is provided in type theories extended with Dybjer's schema for simultaneous inductive-recursive definitions. The technique applies also to the formalisation of partial functions as proper type-theoretic functions, rather than relations representing their graphs.},

year={2001},

keywords={general recursion, nested recursion, partial functions, type theory},

}

** RefWorks **

RT Conference Proceedings

SR Print

ID 47408

A1 Bove, Ana

A1 Capretta, Venanzio

T1 Nested General Recursion and Partiality in Type Theory

YR 2001

T2 Theorem Proving in Higher Order Logics

SN 3-540-42525-X

SP 121

AB We extend Bove's technique for formalising simple general recursive algorithms in constructive type theory to nested recursive algorithms. The method consists in defining an inductive domain predicate, that characterises the inputs on which the algorithm terminates. As a result, the type-theoretic version of the algorithm can be defined by structural recursion on the proof that the input values satisfy this predicate. This technique results in definitions in which the computational and logical parts are clearly separated; hence, the type-theoretic version of the algorithm is given by its purely functional content, similarly to the corresponding program in a functional programming language. In the case of nested recursion, the special predicate and the type-theoretic algorithm must be defined simultaneously, because they depend on each other. This kind of definitions is not allowed in ordinary type theory, but it is provided in type theories extended with Dybjer's schema for simultaneous inductive-recursive definitions. The technique applies also to the formalisation of partial functions as proper type-theoretic functions, rather than relations representing their graphs.

LA eng

OL 30