  It is well known that general recursion cannot be expressed within
Martin-Loef's type theory and various approaches have been proposed to overcome
this problem still maintaining the termination of the computation of the
typable terms. In this work we propose a new approach to this problem based on
the use of inductively generated formal topologies.
