Por favor, use este identificador para citar o enlazar este ítem:
https://hdl.handle.net/20.500.12008/25864
Cómo citar
Registro completo de metadatos
Campo DC | Valor | Lengua/Idioma |
---|---|---|
dc.contributor.author | Peratto, Patricia | - |
dc.date.accessioned | 2020-11-12T18:43:29Z | - |
dc.date.available | 2020-11-12T18:43:29Z | - |
dc.date.issued | 1991 | - |
dc.identifier.citation | Peratto, P. Course-of-values recursion in Martin-Löf's type theory [en línea]. Tesis de maestría. Montevideo : Udelar. FI. INCO - PEDECIBA, 1991. | es |
dc.identifier.uri | https://hdl.handle.net/20.500.12008/25864 | - |
dc.description | Technical Report INCO-91-04 | es |
dc.description.abstract | To facilitate reasoning about programs in Martin Löf’s Type Theory, the introduction general recursion operators has been studied. This allow a more conventional programming style, being possible to separte the termination proof of the program from the proof of other properties. This work experiments with this idea studying Course-of-Values induction for Natural Numbers. An introduction rule is derived from natural induction, obtaining an expression for a recursion operator. A propositional equality that expresses the behavior of the obtained operator is proved. This equality will be usefull when proving properties of programs. ALF is used as editor of Martin Löf’s monomorphic Set Theory and checker of all the proofs. | es |
dc.format.extent | 38 p. | es |
dc.format.mimetype | application/pdf | es |
dc.language.iso | en | es |
dc.publisher | Udelar.FI. | es |
dc.rights | Las obras depositadas en el Repositorio se rigen por la Ordenanza de los Derechos de la Propiedad Intelectual de la Universidad de la República.(Res. Nº 91 de C.D.C. de 8/III/1994 – D.O. 7/IV/1994) y por la Ordenanza del Repositorio Abierto de la Universidad de la República (Res. Nº 16 de C.D.C. de 07/10/2014) | es |
dc.subject | Teoria de tipos | es |
dc.subject | Logical frameworks | es |
dc.subject | Alf | es |
dc.title | Course-of-values recursion in Martin-Löf's type theory | es |
dc.type | Tesis de maestría | es |
dc.contributor.filiacion | Peratto Patricia, Universidad de la República (Uruguay). Facultad de Ingeniería. | - |
thesis.degree.grantor | Universidad de la República (Uruguay). Facultad de Ingeniería | es |
thesis.degree.name | Magíster en Informática | es |
dc.rights.licence | Licencia Creative Commons Atribución - No Comercial - Sin Derivadas (CC - By-NC-ND 4.0) | es |
Aparece en las colecciones: | Tesis de posgrado - Instituto de Computación |
Ficheros en este ítem:
Fichero | Descripción | Tamaño | Formato | ||
---|---|---|---|---|---|
PER91.pdf | Tesis de Maestría | 19,47 MB | Adobe PDF | Visualizar/Abrir |
Este ítem está sujeto a una licencia Creative Commons Licencia Creative Commons