english Icono del idioma   español Icono del idioma  

  1. Colibri
  2. Facultad de Ingeniería
  3. Instituto de Computación
  4. Tesis de posgrado
Por favor, use este identificador para citar o enlazar este ítem: https://hdl.handle.net/20.500.12008/2912 Cómo citar
Registro completo de metadatos
Campo DC Valor Lengua/Idioma
dc.contributor.authorBove, Anaes
dc.date.accessioned2014-11-24T22:35:28Z-
dc.date.available2014-11-24T22:35:28Z-
dc.date.issued1995es
dc.date.submitted20141202es
dc.identifier.citationBOVE, 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.es
dc.identifier.urihttp://hdl.handle.net/20.500.12008/2912-
dc.description.abstractWe 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.es
dc.format.extent49 p.es
dc.format.mimetypeapplication/pdfes
dc.languageenes
dc.publisherUR. FI-INCO,es
dc.rightsLas 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.subjectPROGRAMACION FUNCIONALes
dc.subjectALFes
dc.subjectTEORIA DE TIPOSes
dc.subjectTYPE THEORYes
dc.subjectFUNCTIONAL PROGRAMMINGes
dc.titleA machine assisted proof of the subject reduction property for small typed functional language. Master Thesises
dc.typeTesis de maestríaes
thesis.degree.grantorUniversidad de la República (Uruguay). Facultad de Ingeniería. Instituto de Computación – PEDECIBAes
thesis.degree.nameMagíster en Informáticaes
dc.rights.licenceLicencia 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   
tesis-bove.pdf294,36 kBAdobe PDFVisualizar/Abrir
Mostrar el registro sencillo del ítem


Este ítem está sujeto a una licencia Creative Commons Licencia Creative Commons Creative Commons