General Recursion and Formal Topology
Logic in Computer Science
2010-12-23 v1
Abstract
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.
Keywords
Cite
@article{arxiv.1012.4899,
title = {General Recursion and Formal Topology},
author = {Claudio Sacerdoti Coen and Silvio Valentini},
journal= {arXiv preprint arXiv:1012.4899},
year = {2010}
}
Comments
In Proceedings PAR 2010, arXiv:1012.4555