Differences
This shows you the differences between two versions of the page.
Next revision | Previous revisionNext revisionBoth sides next revision | ||
teaching:cc5115 [2020/02/10 12:08] – created folmedo | teaching:cc5115 [2020/02/10 12:50] – [Motivación y Objetivos] folmedo | ||
---|---|---|---|
Line 1: | Line 1: | ||
- | ====== | + | ====== |
==== Motivación y Objetivos | ==== Motivación y Objetivos | ||
- | Los problemas en las piezas de software pueden acarrear consecuencias catastróficas, | + | El propósito |
+ | |||
+ | Lenguajes populares como Java, JavaScript o Scala han sabido explotar estas características adoptando un enfoque multi-paradigma. Para los objetivos de este utilizaremos sin embargo Haskell, un lenguaje puramente funcional. Haskell se considera en la frontera del diseño de lenguajes de programación y hoy en día tiene una penetración no menor en la industria, siendo usado por compañías como Microsoft, Facebook, IBM, Galois, AT& | ||
- | En este curso estudiaremos | + | A lo largo del curso cubriremos tanto la práctica como la teoría de la programación funcional. Al finalizar |
+ | * escribir | ||
+ | * explotar un sistema de tipos estático, de características avanzadas; | ||
+ | * hacer un uso sofisticado | ||
+ | * reconocer, encapsular y explotar diversos patrones | ||
+ | * escribir | ||
+ | * reconocer y explotar diversas oportunidades de optimización, | ||
+ | * testear programas de manera automática, | ||
- | A lo largo del curso presentaremos los fundamentos matemáticos subyacentes a dichas herramientas, | + | Para un listado más detallado de los tópicos |
- | + | ||
- | + | ||
- | ==== Contenido | + | |
- | Al término del curso, el estudiante manejará las nociones de: | + | |
- | * **Semántica formal de programas: | + | |
- | * **Verificación formal de programas:** será capaz de demostrar (en el sentido matemático) la corrección funcional de un programa mediante el uso de lógica de Hoare y razonar también sobre programas que manipulan estructuras de datos dinámicas mediante el uso de lógica de separación. | + | |
- | * **Análisis estático de programas:** será capaz de razonar formalmente sobre propiedades más generales de los programas, de manera completamente automática, | + | |
==== Elegibilidad ==== | ==== Elegibilidad ==== | ||
- | Curso electivo para Doctorado en Computación, | + | Curso electivo para Ingeniería Civil en Computación. |
==== Requisitos | ==== Requisitos | ||
- | CC4101 Lenguajes | + | Algoritmos y estructura |