Show simple item record

Professor Advisordc.contributor.advisorTanter, Eric
Professor Advisordc.contributor.advisorToro Ipinza, Matías
Authordc.contributor.authorMosso Chávez, Fabián Andrés 
Associate professordc.contributor.otherHevia Angulo, Alejandro
Associate professordc.contributor.otherHitschfeld Kahler, Nancy
Associate professordc.contributor.otherMendoza Rocha, Marcelo
Admission datedc.date.accessioned2020-09-11T13:42:01Z
Available datedc.date.available2020-09-11T13:42:01Z
Publication datedc.date.issued2020
Identifierdc.identifier.urihttps://repositorio.uchile.cl/handle/2250/176770
General notedc.descriptionTesis para optar al grado de Magíster en Ciencias, Mención Computaciónes_ES
General notedc.descriptionMemoria para optar al título de Ingeniero Civil en Computación
Abstractdc.description.abstractMuchos programas realizan operaciones tales como mutar el heap, imprimir en pantalla, leer archivos, comunicarse con otros programas o generar números aleatorios. Estas interacciones son conocidas como efectos colaterales. Los efectos son útiles, pero pueden ser problemáticos: un programa podría sobre-escribir un archivo importante, o un programa podría contener logs de depuración en la etapa de producción, exponiendo información interna. Por lo tanto, existen técnicas como los sistemas de tipos y efectos, que nos permiten razonar estáticamente sobre programas con efectos. En esta tesis, proponemos un cálculo formal con un sistema de efectos que permite a los programadores razonar sobre efectos que podrían y que deben suceder cuando un programa se ejecuta. El sistema de efectos diferencia entre efectos que podrían suceder y efectos que deben suceder. Adicionalmente el sistema de efectos nos permite restringir el número de veces que un efecto puede o debe realizarse durante la ejecución de un programa. El lenguaje presentado en esta tesis es llamado lambda mme-p, donde mme representa a los efectos opcionales y a los efectos obligatorios (may-must effects), y p representa efectos polimórficos, efectos genéricos que son representado por variables de efecto, y estas variables pueden ser reemplazadas por efectos concretos. El trabajo de esta tesis consiste en dos partes. En la primera parte, definimos lambda mme-p, un cálculo formal con un sistema de tipo y efectos que combina tanto los efectos que podrían realizarse como los efectos que deben realizarse, y polimorfismo de efectos. La novedad de este trabajo consiste en la combinación de estos conceptos. En la segunda parte, desarrollamos el formalismo de lambda mme-p junto con la definición y prueba de la propiedad de coherencia (soundness) de su sistema de tipo y efectos. La propiedad de coherencia declara que la semántica estática de lambda mme-p es una aproximación acertada de la semántica dinámica, es decir, una función bien tipada respeta la especificación de efectos (sus privilegios y obligaciones). El trabajo realizado se válida mediante la definición y demostración de la propiedad de coherencia. Esta propiedad indica que el lenguaje propuesto tiene sentido, que el lenguaje indica los efectos que podrían y que deben suceder cuando un programa bien tipado se ejecuta. El sistema de tipos y efectos de lambda mme-p, le permite al programador diseñar y cumplir especificaciones mas fuertes de las que son posibles expresar en un sistema de efectos simple. A pesar que lambda mme-p es mas expresivo que un sistema de efectos simple, aun no hay una implementación del lenguaje. lambda mme-p tiene limitantes, tal como la falta de recursión, o tipos dependientes. Por lo tanto, lambda mme-p aun no seria útil para un programador.es_ES
Patrocinadordc.description.sponsorshipProyecto FONDECYT Regular 1150017es_ES
Lenguagedc.language.isoenes_ES
Publisherdc.publisherUniversidad de Chilees_ES
Type of licensedc.rightsAttribution-NonCommercial-NoDerivs 3.0 Chile*
Link to Licensedc.rights.urihttp://creativecommons.org/licenses/by-nc-nd/3.0/cl/*
Keywordsdc.subjectSistema de efectoses_ES
Keywordsdc.subjectPL/1 (Lenguaje de programación para computadores)es_ES
Títulodc.titleCountable polymorphic may-must effectses_ES
Document typedc.typeTesis
Catalogueruchile.catalogadorgmmes_ES
Departmentuchile.departamentoDepartamento de Ciencias de la Computaciónes_ES
Facultyuchile.facultadFacultad de Ciencias Físicas y Matemáticases_ES
uchile.titulacionuchile.titulacionDoble Titulaciónes_ES


Files in this item

Icon
Icon

This item appears in the following Collection(s)

Show simple item record

Attribution-NonCommercial-NoDerivs 3.0 Chile
Except where otherwise noted, this item's license is described as Attribution-NonCommercial-NoDerivs 3.0 Chile