General Recursion and Formal Topology

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...

Full description

Bibliographic Details
Main Authors: Silvio Valentini, Claudio Sacerdoti Coen
Format: Article
Language:English
Published: Open Publishing Association 2010-12-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1012.4899v1