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

**Harvard**

Bove, A. och Capretta, V. (2008) *A Type of Partial Recursive Functions*.

** BibTeX **

@conference{

Bove2008,

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

title={A Type of Partial Recursive Functions},

booktitle={Theorem Proving in Higher Order Logics, 21st International Conference TPHOLs 2008},

isbn={978-3-540-71065-3},

pages={102--117},

abstract={Our goal is to define a type of partial recursive functions in constructive type theory. In a series of previous articles, we studied two different formulations of partial functions and general recursion. We could obtain a type only by extending the theory with either an impredicative universe or with coinductive definitions. Here we present a new type constructor that eludes such entities of dubious constructive credentials.
We start by showing how to break down a recursive function definition into three components: the first component generates the arguments of the recursive calls, the second evaluates them, and the last computes the output from the results of the recursive calls. We use this dissection as the basis for the introduction rule of the new type constructor.
Every partial recursive function is associated with an inductive domain predicate; evaluation of the function requires a proof that the input values satisfy the predicate.
We give a constructive justification for the new construct by interpreting it into the base type theory. This shows that the extended theory is consistent and constructive.},

year={2008},

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

}

** RefWorks **

RT Conference Proceedings

SR Print

ID 73656

A1 Bove, Ana

A1 Capretta, Venanzio

T1 A Type of Partial Recursive Functions

YR 2008

T2 Theorem Proving in Higher Order Logics, 21st International Conference TPHOLs 2008

SN 978-3-540-71065-3

SP 102

AB Our goal is to define a type of partial recursive functions in constructive type theory. In a series of previous articles, we studied two different formulations of partial functions and general recursion. We could obtain a type only by extending the theory with either an impredicative universe or with coinductive definitions. Here we present a new type constructor that eludes such entities of dubious constructive credentials.
We start by showing how to break down a recursive function definition into three components: the first component generates the arguments of the recursive calls, the second evaluates them, and the last computes the output from the results of the recursive calls. We use this dissection as the basis for the introduction rule of the new type constructor.
Every partial recursive function is associated with an inductive domain predicate; evaluation of the function requires a proof that the input values satisfy the predicate.
We give a constructive justification for the new construct by interpreting it into the base type theory. This shows that the extended theory is consistent and constructive.

LA eng

OL 30