Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Next revision
Previous revision
Last revision Both sides next revision
teaching:cc5115 [2020/02/10 12:08]
folmedo created
teaching:cc5115 [2020/02/10 13:15]
folmedo [Objetivos y contenido]
Line 1: Line 1:
-====== ​Análisis y Verificación de Programas ​(CC7126) ======+====== ​Programación funcional ​(CC5115) ======
  
  
-==== Motivación y Objetivos ​ ====+==== Motivación, objetivos ​contenido ​ ====
  
-Los problemas en las piezas de software pueden acarrear consecuencias catastróficas,​ tanto a nivel económico como de la seguridad de las personas. La validación y verificación de software juegan, ​por lo tanto, ​un rol fundamental en el proceso ​de desarrollo. En particular, para el proceso de verificación se ha recurrido históricamente a diversas técnicas de //testing//. Si bien el testing representa un enfoque muy eficiente para detectar bugssu alcance está limitado a probar ​la //presencia// de bugs, y no su //ausencia//. +El objetivo ​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óny tres características que la hacen particularmente atractiva son su conveniencia ​para //verificar// programasrazonando 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.
  
-En este curso estudiaremos ​el análisis y verificación formal ​de programas, ​que constituyen ​un conjunto ​de herramientas matemáticas ​para razonar //​formalmente//​ sobre el comportamiento ​de los programas. A diferencia del testing, su empleo permite //​demostrar//​--en el sentido matemático--que los programas son correctos y se adhieren a su especificación+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áticode 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.
  
-A lo largo del curso presentaremos ​los fundamentos matemáticos subyacentes a dichas herramientas,​ reconociendo, ​en particular, sus alcances y limitaciones. Estudiaremos,​ además, las distintas estrategias que se utilizan para automatizar su aplicación.  +Para un listado más detallado de los temas abordados ​en el curso consultar ​el {{teaching:cc5115:programa_cc5115.pdf|programa ​del curso}}Para una discusión más a fondo sobre la relevancia y beneficios ​de la programación ​funcional ​consultar ​el artículo {{teaching:​cc5115:​whyfp90.pdf|Why functional programming matters}}.
- +
- +
-==== Contenido ​ ==== +
-Al término del cursoel estudiante manejará las nociones de +
-  * **Semántica formal de programas:** reconocerá dos estrategias clásicas para describir rigurosamente el significado o efecto de un programa. ​ +
-  * **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,​ y en tiempo de compilación.+
  
  
 ==== Elegibilidad ==== ==== Elegibilidad ====
-Curso electivo para Doctorado en Computación,​ Magíster en Ciencias de la Computación e Ingeniería Civil en Computación.+Curso electivo para Ingeniería Civil en Computación.
  
  
 ==== Requisitos ​ ==== ==== Requisitos ​ ====
-CC4101 Lenguajes ​de Programación / Autorización ​(contactar [[folmedo@dcc.uchile.cl|Federico]]).\\ El curso no presenta ningún requisito adicional, aunque será de gran ayuda  cierto grado de madurez matemática por parte del alumno.+Algoritmos y estructura ​de datos (CC3001) y matemáticas discretas para la computación (CC3101). 
  
  
Line 32: Line 35:
 ==== Material ​ ==== ==== Material ​ ====
  
-  * G. Winskel, ​//The Formal Semantics of Programming Languages//,​ MIT Press, 1993 ([[https://uchile-primo.hosted.exlibrisgroup.com/​primo-explore/​fulldisplay?​docid=uchile_alma21142459530003936&​context=L&​vid=56UDC_INST&​search_scope=uchile_scope&​tab=uchile_tab&​lang=es_CL|disponible en biblioteca]]) +  * //Learn you a Haskell for great goodA beginner'​s guide//. Lipovača M., No Starch Press1º  Edición2011. ([[http://learnyouahaskell.com|disponible ​online]])   
-  * F. Nielson et al., //Semantics with Applications:​ An Appetizer//Springer2007 ([[https://uchile-primo.hosted.exlibrisgroup.com/​primo-explore/​fulldisplay?​docid=uchile_alma51170845280003936&​context=L&​vid=56UDC_INST&​search_scope=uchile_scope&​tab=uchile_tab&​lang=es_CL|disponible ​en biblioteca]]) +  * //Programming in Haskell//. HuttonGCambridge University Press2º Edición, 2016. ([[http://www.cs.nott.ac.uk/~pszgmh/pih.html|disponible online]])  
-  * F. Nielson et al., //Principles of Program Analysis//, Springer, 2015 ([[https://​uchile-primo.hosted.exlibrisgroup.com/​primo-explore/​fulldisplay?​docid=uchile_alma21123471330003936&​context=L&​vid=56UDC_INST&​search_scope=uchile_scope&​isFrbr=true&​tab=uchile_tab&​lang=es_CL|disponible en biblioteca]]) +  * //Thinking functionally with Haskell//. Richard Bird. Cambridge University Press. ​1º Edición2015.
-  * P.WO'​Hearn,​ //A Primer on Separation Logic (and Automatic Program Verification and Analysis)//,​ Notas de la Escuela de Verano Marktoberdorf 2011 ([[http://www0.cs.ucl.ac.uk/staff/p.ohearn/​papers/​Marktoberdorf11LectureNotes.pdf|disponible online]]) +
-  * J. B. Almeida et al., //Rigorous Software Development:​ An Introduction to Program Verification//, Springer, 2011 +
-  * AAppel et al., //Program Logics for Certified Compilers//, ​Cambridge University Press, 2014 +
-  * PCousot//A Tutorial on Abstract Interpretation//,​ VMCAI'​05 Industrial Day on Automatic Tools for Program Verification,​ 2005 ([[https://​homepage.cs.uiowa.edu/​~tinelli/​classes/​seminar/​|disponible online]]) +
- +
 ==== Contacto ==== ==== Contacto ====
 Federico Olmedo, Oficia 311N, [[folmedo@dcc.uchile.cl|email]] Federico Olmedo, Oficia 311N, [[folmedo@dcc.uchile.cl|email]]