|
|
|
|
| LEADER |
00000nam a2200000 4500 |
| 003 |
AR_CdUFM |
| 005 |
20171023134829.0 |
| 008 |
110819s2005 ag_||||| |||| 00| 0 spa d |
| 952 |
|
|
|0 0
|1 0
|2
|4 0
|6 TE_C_PAS_EJ_2_000000000000000
|7 0
|9 17769
|a MMA
|b MMA
|c DEPOSITO
|d 2006-03-04
|e Donación del autor
|o TE C PAS ej.2
|p 18024
|r 2017-07-21 00:00:00
|t 2
|w 2011-08-19
|y TRAB. ESP.
|
| 952 |
|
|
|0 0
|1 0
|2
|4 0
|6 TRABAJO_ESPECIAL_COMPUTACIÓN_CAJA_5_000000000000000__18023
|7 0
|9 17770
|a MMA
|b MMA
|c 94
|d 2006-03-04
|e Donación del autor
|l 2
|m 3
|o Trabajo Especial Computación CAJA 5 - 18023
|p 18023
|r 2017-07-21 00:00:00
|s 2012-09-04
|t 1
|w 2011-08-19
|x TE C PAS
|y TRAB. ESP.
|
| 999 |
|
|
|c 13544
|d 13544
|
| 040 |
|
|
|a AR_CdUFM
|c AR_CdUFM
|
| 100 |
1 |
|
|9 13070
|a Pastawski, Fernando Martín,
|d 1982-
|
| 245 |
1 |
0 |
|a Inferencia de tipos para Fˆ, un λ cálculo polimórfico con terminación basada en tipos /
|c Fernando Martín Pastawski.
|
| 260 |
|
|
|a [S.l. :
|b s.n.],
|c 2005.
|
| 300 |
|
|
|a 43 h. :
|b il. ;
|c 30 cm.
|
| 500 |
|
|
|a Incluye glosario.
|
| 502 |
|
|
|a Tesis (Lic. en Ciencias de la Computación)--Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física, 2005.
|
| 504 |
|
|
|a Incluye referencias bibliográficas : h. 42-43.
|
| 520 |
|
|
|a 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.
|
| 590 |
|
|
|a La biblioteca posee ej.
|
| 650 |
|
4 |
|a Theory of computation.
|
| 650 |
|
4 |
|a Logic and meaning of programs.
|
| 650 |
|
4 |
|a Lógica y significado de programas.
|
| 650 |
|
4 |
|a Mathematical logic and formal languages.
|
| 650 |
|
4 |
|a Lambda calculus and related systems.
|
| 650 |
|
4 |
|a Cálculo de Lambda y sistemas relacionados.
|
| 650 |
|
4 |
|a Computability theory.
|
| 650 |
|
4 |
|a Computational logic.
|
| 650 |
|
4 |
|a Mechanical theorem proving.
|
| 653 |
|
|
|a Type Theory.
|
| 653 |
|
|
|a Type Checking.
|
| 653 |
|
|
|a Tipos con tamaños.
|
| 653 |
|
|
|a Terminación.
|
| 653 |
|
|
|a Recursión.
|
| 653 |
|
|
|a Type inference.
|
| 653 |
|
|
|a Sized types.
|
| 653 |
|
|
|a Termination.
|
| 653 |
|
|
|a Recursion.
|
| 653 |
|
|
|a Type based termination.
|
| 653 |
|
|
|a Teoría de Tipos.
|
| 653 |
|
|
|a Inferencia de tipos.
|
| 700 |
1 |
|
|9 1078
|a Barthe, Gilles,
|d 1967- ,
|e dir.
|
| 700 |
1 |
|
|9 5595
|a Fridlender, Daniel Edgardo,
|d 1964- ,
|e dir.
|
| 942 |
|
|
|c TRAB. ESP.
|2
|
| 945 |
|
|
|a MBO
|d 2006-03-01
|
| 945 |
|
|
|a MBO
|d 2011-08-19
|
