Por favor, use este identificador para citar o enlazar este ítem:
https://hdl.handle.net/20.500.12008/2912
Cómo citar
| Título: | A machine assisted proof of the subject reduction property for small typed functional language. Master Thesis |
| Autor: | Bove, Ana |
| 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. Instituto de Computación – PEDECIBA |
| Tipo: | Tesis de maestría |
| Palabras clave: | PROGRAMACION FUNCIONAL, ALF, TEORIA DE TIPOS, TYPE THEORY, FUNCTIONAL PROGRAMMING |
| Fecha de publicación: | 1995 |
| Resumen: | We present an experiment in formally describing a programming language and its properties in constructive type theory. By constructive type theory we understand primarily the formulation of Martin Löf's set theory. Constructive type theory can also be seen as a programming language where we write types, and objects of these types can be view as funtional programming environments of proof assistants. The language we analyze is a small typed functional language. We present its syntax, its dynamic semanctics and its type system. Among other properties, we present a formalization pf the Subject Reduction property for the language. The proof assistant we use is ALF. |
| Editorial: | UR. FI-INCO, |
| Citación: | BOVE, A. "A machine assisted proof of the subject reduction property for small typed functional language. Master Thesis". Tesis de maestría, Universidad de la República (Uruguay). Facultad de Ingeniería. Instituto de Computación – PEDECIBA, 1995. |
| Licencia: | Licencia Creative Commons Atribución – No Comercial – Sin Derivadas (CC BY-NC-ND 4.0) |
| Aparece en las colecciones: | Tesis de posgrado - Instituto de Computación |
Ficheros en este ítem:
| Fichero | Descripción | Tamaño | Formato | ||
|---|---|---|---|---|---|
| tesis-bove.pdf | 294,36 kB | Adobe PDF | Visualizar/Abrir |
Este ítem está sujeto a una licencia Creative Commons Licencia Creative Commons
