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.
General Recursion and Formal Topology / C. Sacerdoti Coen; S. Valentini. - ELETTRONICO. - 43:(2010), pp. 65-75. (Intervento presentato al convegno Workshop on Partiality and Recursion in Interactive Theorem Provers (PAR 2010) tenutosi a Edinburgh nel 15th July 2010).
General Recursion and Formal Topology
SACERDOTI COEN, CLAUDIO;
2010
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.File in questo prodotto:
Eventuali allegati, non sono esposti
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
