期刊名称：Electronic Proceedings in Theoretical Computer Science
电子版ISSN：2075-2180
出版年度：2010
卷号：43
页码：65-75
DOI：10.4204/EPTCS.43.5
出版社：Open Publishing Association
摘要：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.
