000			03326nam a2200265 a 4500
003			AR-LpUFIB
005			20240131171202.0
007			ta
008			230201s2020 ag dom 000 0 spa d
024	8		_aDIF007165
040			_aAR-LpUFIB _bspa _cAR-LpUFIB
100	1		_aSottile, Cristian _9258129
245	1	0	_aAgregando polimorfismo a una lógica que identifica proposiciones isomorfas
300			_a1 archivo (3,1 MB)
502			_a Tesina (Licenciatura en Informática) - Universidad Nacional de La Plata. Facultad de Informática, 2020.
505	0		_a 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
650		4	_aCÁLCULO LAMBDA _9253468
650		4	_aPOLIMORFISMO _9253797
653			_ateoría de tipos
700	1		_aDíaz Caro, Alejandro , _eDirector/a _9255694
700	1		_aPons, Claudia Fabiana , _eCodirector/a _9251525
856	4	0	_uhttp://sedici.unlp.edu.ar/handle/10915/118544
856	4	0	_u http://catalogo.info.unlp.edu.ar/meran/getDocument.pl?id=2397
942			_cTE
999			_c849178 _d849178