Título:
Course-of-values recursion in Martin-Löf's type theory
Otros títulos:
Coordinador:
Director:
Compilador:
Autor:
Peratto, Patricia
Tutor:
Tipo de documento:
Tesis de maestría
Editor:
Palabras clave:
Teoria de tipos
Logical frameworks
Alf
Logical frameworks
Alf
Descriptores:
Año de publicación:
1991
Contenido:
Resumen:
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.
Descripción:
Technical Report INCO-91-04
Editorial:
Udelar.FI.
EN:
Financiadores:
Citación:
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.
Citación:
metadata.cc.license.name:
Documento del Gobiberno:
URI:
https://hdl.handle.net/20.500.12008/25864
ISBN:
e-ISBN:
ISSN:
ISMN:
Otros identificadores:
Título Obtenido:
Magíster en Informática
Facultad o Servicio que otorga el Título:
Universidad de la República (Uruguay). Facultad de Ingeniería
Licencia:
Licencia Creative Commons Atribución - No Comercial - Sin Derivadas (CC - By-NC-ND 4.0)
Cobertura geográfica:
Cobertura temporal:
metadata.dc.relation.IsVersionOf:
Clasificación:
Es versión de:
Colecciones:
| Ficheros | Descripción | Tamaño | Formato | ||
|---|---|---|---|---|---|
| PER91.pdf | Tesis de Maestría | 19.01 MB | Adobe PDF |