This is an old revision of the document!


Programación funcional (CC5115)

Motivación y Objetivos

El propósito de este curso es introducir la programación funcionalº a través del lenguaje Haskell. La programación funcional es reconocida por dar lugar a un estilo mucho más declarativo –y elegante– de programación, y tres características que la hacen particularmente atractiva son su conveniencia para verificar programas, razonando algebraicamente de la misma manera que lo hacemos en matemática, para paralelizar la ejecución de programas, ganando órdenes de magnitud en eficiencia, y por último, para abstraer patrones de programación recurrentes, generando código más compacto, robusto y reusable.

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&T, JaneStreet y la NASA.

A lo largo del curso cubriremos tanto la práctica como la teoría de la programación funcional. Al finalizar el mismo, los estudiantes serán capaces de:

  • escribir programas funcionales usando el lenguaje Haskell;
  • explotar un sistema de tipos estático, de características avanzadas;
  • hacer un uso sofisticado de la recursión, para resolver problemas no-triviales;
  • reconocer, encapsular y explotar diversos patrones de programación recurrentes;
  • escribir programas que se ejecutan de manera paralela;
  • reconocer y explotar diversas oportunidades de optimización, y
  • testear programas de manera automática, usando la librería QuickCheck.

Para un listado más detallado de los temas abordados en el curso consultar el programa del curso (CC5115). Para una discusión más a fondo sobre la relevancia y beneficios de la programación funcional consultar el artículo Why functional programming matters.

Elegibilidad

Curso electivo para Ingeniería Civil en Computación.

Requisitos

Algoritmos y estructura de datos (CC3001) y matemáticas discretas para la computación (CC3101).

Evaluación

Evaluación continua a través de tareas y una presentación oral (en base a un artículo o capítulo de libro). No habrá controles.

Material

  • G. Winskel, The Formal Semantics of Programming Languages, MIT Press, 1993 (disponible en biblioteca)
  • F. Nielson et al., Semantics with Applications: An Appetizer, Springer, 2007 (disponible en biblioteca)
  • F. Nielson et al., Principles of Program Analysis, Springer, 2015 (disponible en biblioteca)
  • P.W. O'Hearn, A Primer on Separation Logic (and Automatic Program Verification and Analysis), Notas de la Escuela de Verano Marktoberdorf 2011 (disponible online)
  • J. B. Almeida et al., Rigorous Software Development: An Introduction to Program Verification, Springer, 2011
  • A. Appel et al., Program Logics for Certified Compilers, Cambridge University Press, 2014
  • P. Cousot, A Tutorial on Abstract Interpretation, VMCAI'05 Industrial Day on Automatic Tools for Program Verification, 2005 (disponible online)

Contacto

Federico Olmedo, Oficia 311N, email