SITIO DE TEST - SITIO DE TEST - SITIO DE TEST - SITIO DE TEST - SITIO DE TEST - SITIO DE TEST - SITIO DE TEST - SITIO DE TEST - SITIO DE TEST
 

Formalización de Sistema I con tipo Top

Vista sencilla de ítem
dc.contributor.advisorManzino, Cecilia
dc.contributor.coadvisorSottile, Cristian
dc.creatorSettimo, Agustín Francisco
dc.date.accessioned2024-05-13T18:42:53Z
dc.date.available2024-05-13T18:42:53Z
dc.date.issued2023-11
dc.description.abstractLos sistemas de tipos desempeñan un papel esencial en la garantía del comportamiento adecuado de los programas. Sin embargo, estos imponen cierta rigidez a la hora de escribir dichos programas, ya que se deben adherir estrictamente a las reglas de tipado establecidas. Existen una serie de “sistemas módulo isomorfismos” [DD19; DD23; AD20; DM15; Sot20; SDM20] que proponen flexibilizar esta restricción considerando aquellos tipos que sean isomorfos como idénticos. En simples palabras, dos tipos se consideran isomorfos cuando es posible convertir uno en el otro, y viceversa, sin perder información en el proceso. Es decir, si dos tipos A y B son isomorfos, es posible usar un término de tipo A en cualquier lugar que se espere un término de tipo B aplicando la conversión correspondiente. Trabajar con tipos isomorfos provee mayor flexibilidad en la construcción de programas y permite combinarlos de formas que normalmente no serían posibles. Este trabajo se centra principalmente en el primero de estos sistemas, llamado Sistema I. Aquí, se presenta una formalización de una adaptación de dicho sistema en el lenguaje Agda, además, se añade el tipo Top y los isomorfismos correspondientes para ampliar aún más la flexibilidad del sistema. Esta formalización va acompañada de pruebas formales que demuestran el cumplimiento de diversas propiedades, siendo la normalización fuerte una de las más cruciales. Es importante destacar que la prueba de normalización fuerte utiliza la técnica de logical relations pero con predicados distintos a los presentados en la prueba de candidatos de reducibilidad de Girard.
dc.description.filFil: Settimo, Agustín Francisco. Universidad Nacional de Rosario. Facultad de Ciencias Exactas, Ingeniería y Agrimensura; Argentina.
dc.description.peerreviewedPeer reviewed
dc.description.versionpeerreviewed
dc.identifier.urihttps://hdl.handle.net/2133/27028
dc.language.isoes
dc.rightsopenAccess
dc.rights.holderSettimo, Agustín Francisco
dc.rights.textAttribution-ShareAlike 4.0 Internationalen
dc.rights.urihttp://creativecommons.org/licenses/by-sa/4.0/
dc.subjectCálculo lambda
dc.subjectTipos isomorfos
dc.subjectFormalización
dc.subjectAgda
dc.titleFormalización de Sistema I con tipo Top
dc.typetesis
dc.type.collectiontesis
dc.type.othertesis de grado
dc.type.versionacceptedVersion
lom.educational.contextgrado
lom.educational.difficultymediana dificultad
lom.educational.typicalAgeRangeadultos

Archivos

Bloque original
Mostrando 1 - 1 de 1
Miniatura
Nombre:
Tesis de Licenciatura en Ciencias de la Computación. Settimo, Agustin Francisco.pdf
Tamaño:
613.71 KB
Formato:
Adobe Portable Document Format
Descargar
Bloque de licencias
Mostrando 1 - 1 de 1
Nombre:
license.txt
Tamaño:
3.87 KB
Formato:
Item-specific license agreed upon to submission
Descripción:
Descargar

Colecciones

FCEIA-ECEN-DCC- Trabajos Finales de Grado (trabajos finales, proyectos y tesinas)