Local cover image
Local cover image

Agregando polimorfismo a una lógica que identifica proposiciones isomorfas

By: Contributor(s): Material type: TextTextPublication details: 2020Description: 1 archivo (3,1 MB)Subject(s): Online resources:
Contents:
I Introducción y preliminares -- 1 Introducción -- 1.1 Motivación -- 1.2 El cálculo lambda como método de estudio -- 1.3 Nuestro aporte: una extensión polimórfica de Sistema I -- 1.4 Estructura del trabajo -- 2 Introducción al cálculo lambda -- 2.1 Orígenes -- 2.2 Definición -- 2.3 Computación -- 2.3.1 Sistemas de reescritura -- 2.3.2 Reescritura en el calculo lambda -- 2.3.3 Estrategias de reducción -- 3 Cálculo lambda y sistemas de tipos -- 3.1 Sistemas de tipos -- 3.2 Cálculo lambda simplemente tipado -- 3.2.1 El conjunto de los tipos -- 3.2.2 El conjunto de los términos -- 3.2.3 Reglas de tipado -- 3.2.4 Derivaciones de tipos -- 3.2.5 Propiedades de interés -- 3.3 Sistema F -- 3.3.1 Tipos y términos -- 3.3.2 Funciones relevantes -- 3.3.3 Reglas de tipado -- 3.3.4 Reglas de reducción -- 3.3.5 Ejemplos -- 3.4 Extensión con pares -- 4 Computación y Lógica: la correspondencia Curry-Howard -- 4.1 Deducción Natural -- 4.1.1 Definición -- 4.1.2 Construcción de pruebas -- 4.1.3 Simplificación de pruebas -- 4.2 Correspondencia Curry-Howard -- 4.2.1 Definición -- 4.2.2 Simplificación de pruebas y evaluación de programas -- 4.3 Conclusiones -- II Estado del arte -- 5 Isomorfismos en la programación y en la lógica -- 5.1 Definición -- 5.2 Caracterización -- 5.2.1 Cálculo lambda simplemente tipado con pares -- 5.2.2 Sistema F con pares -- 6 Conjunto I: sistemas módulo isomorfismos -- 6.1 Motivación -- 6.1.1 La perspectiva de la programación -- 6.1.2 La perspectiva de la lógica -- 6.2 Internacionalización de isomorfismos -- 6.2.1 Equivalencia entre tipos -- 6.2.2 Reglas de tipado -- 6.2.3 Equivalencia entre términos -- 6.2.4 Relación de reducción -- 6.3 Sistema I -- 6.3.1 Definición -- 6.3.2 Ejemplos -- III Nuestro aporte: Sistema I Polimórfico -- 7 Sistema I Polimórfico -- 7.1 Introducción -- 7.2 Definición -- 7.2.1 Funciones relevantes -- 7.2.2 Equivalencia entre tipos -- 7.2.3 Reglas de tipado -- 7.2.4 Equivalencia entre términos -- 7.2.5 Relación de reducción -- 7.3 Ejemplos -- 7.4 Propiedades -- 8 Conclusiones y trabajo futuro -- 8.1 Conclusiones -- 8.2 Trabajo futuro -- 8.2.1 Adición de conectivas -- 8.2.2 Terminación -- 8.2.3 Eta-expansión rule -- 8.2.4 Implementación y punto fijo
Dissertation note: Tesina (Licenciatura en Informática) - Universidad Nacional de La Plata. Facultad de Informática, 2020.
Star ratings
    Average rating: 0.0 (0 votes)
Holdings
Item type Home library Collection Call number URL Status Date due Barcode
Tesis de posgrado Tesis de posgrado Biblioteca de la Facultad de Informática TES 20/72 (Browse shelf(Opens below)) Available DIF-05012
Tesis de posgrado Tesis de posgrado Biblioteca de la Facultad de Informática Biblioteca digital Link to resource No corresponde
Tesis de posgrado Tesis de posgrado Biblioteca de la Facultad de Informática Biblioteca digital Link to resource No corresponde

Tesina (Licenciatura en Informática) - Universidad Nacional de La Plata. Facultad de Informática, 2020.

I Introducción y preliminares -- 1 Introducción -- 1.1 Motivación -- 1.2 El cálculo lambda como método de estudio -- 1.3 Nuestro aporte: una extensión polimórfica de Sistema I -- 1.4 Estructura del trabajo -- 2 Introducción al cálculo lambda -- 2.1 Orígenes -- 2.2 Definición -- 2.3 Computación -- 2.3.1 Sistemas de reescritura -- 2.3.2 Reescritura en el calculo lambda -- 2.3.3 Estrategias de reducción -- 3 Cálculo lambda y sistemas de tipos -- 3.1 Sistemas de tipos -- 3.2 Cálculo lambda simplemente tipado -- 3.2.1 El conjunto de los tipos -- 3.2.2 El conjunto de los términos -- 3.2.3 Reglas de tipado -- 3.2.4 Derivaciones de tipos -- 3.2.5 Propiedades de interés -- 3.3 Sistema F -- 3.3.1 Tipos y términos -- 3.3.2 Funciones relevantes -- 3.3.3 Reglas de tipado -- 3.3.4 Reglas de reducción -- 3.3.5 Ejemplos -- 3.4 Extensión con pares -- 4 Computación y Lógica: la correspondencia Curry-Howard -- 4.1 Deducción Natural -- 4.1.1 Definición -- 4.1.2 Construcción de pruebas -- 4.1.3 Simplificación de pruebas -- 4.2 Correspondencia Curry-Howard -- 4.2.1 Definición -- 4.2.2 Simplificación de pruebas y evaluación de programas -- 4.3 Conclusiones -- II Estado del arte -- 5 Isomorfismos en la programación y en la lógica -- 5.1 Definición -- 5.2 Caracterización -- 5.2.1 Cálculo lambda simplemente tipado con pares -- 5.2.2 Sistema F con pares -- 6 Conjunto I: sistemas módulo isomorfismos -- 6.1 Motivación -- 6.1.1 La perspectiva de la programación -- 6.1.2 La perspectiva de la lógica -- 6.2 Internacionalización de isomorfismos -- 6.2.1 Equivalencia entre tipos -- 6.2.2 Reglas de tipado -- 6.2.3 Equivalencia entre términos -- 6.2.4 Relación de reducción -- 6.3 Sistema I -- 6.3.1 Definición -- 6.3.2 Ejemplos -- III Nuestro aporte: Sistema I Polimórfico -- 7 Sistema I Polimórfico -- 7.1 Introducción -- 7.2 Definición -- 7.2.1 Funciones relevantes -- 7.2.2 Equivalencia entre tipos -- 7.2.3 Reglas de tipado -- 7.2.4 Equivalencia entre términos -- 7.2.5 Relación de reducción -- 7.3 Ejemplos -- 7.4 Propiedades -- 8 Conclusiones y trabajo futuro -- 8.1 Conclusiones -- 8.2 Trabajo futuro -- 8.2.1 Adición de conectivas -- 8.2.2 Terminación -- 8.2.3 Eta-expansión rule -- 8.2.4 Implementación y punto fijo

Click on an image to view it in the image viewer

Local cover image