General Recursion and Formal Topology
Claudio Sacerdoti Coen, Silvio Valentini · EPiC series in computing · 2018
It is well known that general recursion cannot be expressed within Martin-Löf's type theory and that 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.