El Catálogo Colectivo reúne los registros del material que posee cada una de las
bibliotecas de la Universidad Nacional de Córdoba, pudiendo encontrarse colecciones
especializadas y actualizadas en todas las áreas del conocimiento; lo que permite una
amplia visibilidad y garantiza el acceso al patrimonio documental de la Universidad.
Se encuentra disponible para toda la comunidad académica: estudiantes, docentes,
egresados e investigadores.
Si formas parte de la comunidad de la UNC también podés solicitar préstamos de material,
a cualquier biblioteca universitaria, utilizando el servicio de préstamo interbibliotecario,
independientemente de la facultad a la que pertenezcas, la carrera que curses o la cátedra
que dictes.
Inferencia de tipos para Fˆ, un λ cálculo polimórfico con terminación basada en tipos /
El propósito de este trabajo es presentar el cálculo F-sombrero y lograr inferencia de tipos eficiente para el mismo. F-sombrero es un cálculo que resulta de enriquecer el sistema de Girard con anotaciones de tamaño al estilo lambda-sombrero. La particularidad del sistema de tipos F-sombrero, al igu...
El propósito de este trabajo es presentar el cálculo F-sombrero y lograr inferencia de tipos eficiente para el mismo. F-sombrero es un cálculo que resulta de enriquecer el sistema de Girard con anotaciones de tamaño al estilo lambda-sombrero. La particularidad del sistema de tipos F-sombrero, al igual que lambda-sombrero, es que permite acarrear información de tamaño (profundidad de constructores) permitiendo garantizar la normalización fuerte de expresiones bien tipadas. Esta propiedad, junto con un algoritmo de inferencia de tipos, permite garantizar la terminación de programas funcionales estáticamente, más importante aún , garantizar la correctitud de demostraciones inductivas en sistemas que usan el isomorfismo de Curry-Howard.
