Inferencia de tipos para Fˆ, un λ cálculo polimórfico con terminación basada en tipos / Fernando Martín Pastawski.
Detalles de publicación: [S.l. : s.n.], 2005.Descripción: 43 h. : il. ; 30 cmTema(s):- Theory of computation
- Logic and meaning of programs
- Lógica y significado de programas
- Mathematical logic and formal languages
- Lambda calculus and related systems
- Cálculo de Lambda y sistemas relacionados
- Computability theory
- Computational logic
- Mechanical theorem proving
- Type Theory
- Type Checking
- Tipos con tamaños
- Terminación
- Recursión
- Type inference
- Sized types
- Termination
- Recursion
- Type based termination
- Teoría de Tipos
- Inferencia de tipos
| Tipo de ítem | Biblioteca actual | Signatura topográfica | Copia número | Estado | Fecha de vencimiento | Código de barras | Reserva de ítems | |
|---|---|---|---|---|---|---|---|---|
Trabajo Especial de Grado
|
FaMAF Secc. Tesis y Trabajos especiales | Trabajo Especial Computación CAJA 5 - 18023 | 1 | Disponible | 18023 | |||
|
Trabajo Especial de Grado
|
FaMAF Depósito Interno | TE C PAS ej.2 | 2 | Disponible | 18024 |
Incluye glosario.
Tesis (Lic. en Ciencias de la Computación)--Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física, 2005.
Incluye referencias bibliográficas : h. 42-43.
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.
Haga clic en una imagen para verla en el visor de imágenes