CRIS Current Research Information System
IRIS è la soluzione IT che facilita la raccolta e la gestione dei dati relativi alle attività e ai prodotti della ricerca. Fornisce a ricercatori, amministratori e valutatori gli strumenti per monitorare i risultati della ricerca, aumentarne la visibilità e allocare in modo efficace le risorse disponibili.
EnglishIt 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.
| Titolo: | General Recursion and Formal Topology | |
| Autore/i: | SACERDOTI COEN, CLAUDIO; S. Valentini | |
| Autore/i Unibo: | ||
| Anno: | 2010 | |
| Titolo del libro: | Proceedings Workshop on Partiality and Recursion in Interactive Theorem Provers | |
| Pagina iniziale: | 65 | |
| Pagina finale: | 75 | |
| 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. | |
| Data prodotto definitivo in UGOV: | 27-feb-2011 | |
| Appare nelle tipologie: | 4.01 Contributo in Atti di convegno |
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.
Copyright © 2022