some image logo

HOME

SEARCH

CURRENT ISSUE

REGULAR ISSUES

   Volume 1 (2005)

      Issue 1

      Issue 2

      Issue 3

   Volume 2 (2006)

   Volume 3 (2007)

   Volume 4 (2008)

   Volume 5 (2009)

   Volume 6 (2010)

   Volume 7 (2011)

   Volume 8 (2012)

   Volume 9 (2013)

   Volume 10 (2014)

   Volume 11 (2015)

   Volume 12 (2016)

SPECIAL ISSUES

SURVEY ARTICLES

AUTHORS

ABOUT

SERVICE

LOGIN

FAQ

SUPPORT

CONTACT

VOLUME 1, ISSUE 2, PAPER 1


General recursion via coinductive types

©Venanzio Capretta, University of Ottawa

Abstract
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: Partial(A). We show how this simple device is sufficient to formalize all recursive functions between two given types.

Publication date: July 13, 2005

Full Text: PDF | PostScript
DOI: 10.2168/LMCS-1(2:1)2005

Hit Counts: 12384

Creative Commons