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...
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 |
Similar Items
-
A constructive and formal proof of Lebesgue’s Dominated Convergence Theorem in the interactive theorem prover Matita
by: Claudio Sacerdoti Coen, et al.
Published: (2008-12-01) -
Topological recursion in the Ramond sector
by: Kento Osuga
Published: (2019-10-01) -
Supereigenvalue models and topological recursion
by: Vincent Bouchard, et al.
Published: (2018-04-01) -
DECISION PROBLEMS AND RECURSIVENESS IN FORMAL LOGIC SYSTEMS
by: Iveth Martínez, et al.
Published: (2017-04-01) -
Formal proofs concerning partial recursive functions.
by: Rotenberg, Leo Joseph
Published: (2005)