id: 05200108
dt: j
an: 05200108
au: Capretta, Venanzio
ti: General recursion via coinductive types.
so: Log. Methods Comput. Sci. 1, No. 2, Paper 1, 28 p., electronic only (2005).
py: 2005
pu: Logical Methods in Computer Science c/o Institute of Theoretical Computer
    Science, Technical University of Braunschweig, Braunschweig
la: EN
cc: 
ut: 
ci: 
li: doi:10.2168/LMCS-1(2:1)2005
ab: Summary: We consider the problem of formalizing general recursive functions
    in intensional type theory. The proposed solution exploit coinductive
    types to model infinite computations. Every type $A$ is associated to a
    type of partial elements, Partial$(A)$, coinductively generated by two
    constructors: the first, return$(a)$, just returns an element $a : A$;
    the second, step$(x)$, adds a computation step to a recursive element
    $x : \text{Partial}(A)$. We show how this simple device is sufficient
    to formalize all recursive functions between two given types.
rv: