General Recursion and Formal Topology

Claudio Sacerdoti Coen
(Dipartimento di Scienze dell'Informazione, Università di Bologna)
Silvio Valentini
(Dipartimento di Matematica Pura e Applicata, Università di Padova)

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.

In Ana Bove, Ekaterina Komendantskaya and Milad Niqui: Proceedings Workshop on Partiality and Recursion in Interactive Theorem Provers (PAR 2010), Edinburgh, UK, 15th July 2010, Electronic Proceedings in Theoretical Computer Science 43, pp. 65–75.
Published: 21st December 2010.

ArXived at: https://dx.doi.org/10.4204/EPTCS.43.5 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org