Differences

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

--- teaching:cc7110 [2019/06/07 19:10] – mtoro
+++ teaching:cc7110 [2023/12/18 19:45] (current) – etanter
@@ Line 3: / Line 3: @@
 **Objetivo general**
-El curso entrega los elementos técnicos y formales necesarios para entender la problemática de garantizar que los programas cumplen con sus objetivos, limitando efectos indeseados, lo más temprano posible. Se estudian las nociones de programas válidos, errores y excepciones, contratos, y sobre todo, tipos. En particular, se describen los conceptos fundamentales de los sistemas de tipos, permitiendo entender porque los lenguajes de hoy siguen evolucionando en ese aspecto (por ejemplo, el sistema de tipos de Java), y porque no existe una respuesta única y definitiva al problema. El alumno será capaz además de relacionar un sistema de tipo con la semántica del lenguaje, demostrando su coherencia. Además de proveer un entendimiento más profundo de los lenguajes de programación, el curso habilita a los alumnos para diseñar (extensiones de) lenguajes que proveen garantías fuertes de buen comportamiento.
+El curso entrega los elementos técnicos y formales necesarios para entender la problemática de garantizar que los programas cumplen con sus objetivos, limitando efectos indeseados, lo más temprano posible. Se estudian las nociones de programas válidos, errores y excepciones, contratos, y sobre todo, tipos. En particular, se describen los conceptos fundamentales de los sistemas de tipos, permitiendo entender porque los lenguajes de hoy siguen evolucionando en ese aspecto, y porque no existe una respuesta única y definitiva al problema. El alumno será capaz además de relacionar un sistema de tipo con la semántica del lenguaje, demostrando formalmente su coherencia. Además de proveer un entendimiento más profundo de los lenguajes de programación, el curso habilita a los alumnos para diseñar (extensiones de) lenguajes que proveen garantías fuertes de buen comportamiento.
 //Este curso es parte de los grupos de cursos recomendados para las lineas de especialización en Ciencia de la Computación y en Ingeniería de Software.//
@@ Line 41: / Line 41: @@
 El curso termina con una mini-conferencia donde los estudiantes presentan temas estudiados en base a artículos y/o capítulos de libros.
-** Horario **
+[[teaching:cc7110:2023:presentaciones|Presentaciones 2023]]
-/1: 1.4-3.4
-** Trail 2019/1 **
-    * 18/03: Intro
-    * 20/03: PFPL Cap 1
-    * 25/03: PFPL Cap 2
-    * 27/03: PFPL Cap 3 + ejercicios
-    * **mini-tarea 1** (27/03-07/04)
-    * 01/04: PFPL Cap 4
-    * 03/04: PFPL Cap 5 (hasta 5.2)
-    * 08/04: PFPL Cap 5 y Cap 6 (hasta 6.1)
-    * 10/04: PFPL Cap 6 + corrección mini tarea 1
-    * 15/04: **mini-control 1** + PFPL Cap 7
-    * 17/04: PFPL Cap 8
-    * 22/04: PFPL Cap 10 (menos 10.3), intro Cap 11
-    * **mini-tarea 2** (23/04-30/04)
-    * 24/04: PFPL Cap 11
-    * 29/04: PFPL Cap 12 (statics)
-    * 06/05: PFPL Cap 12 (dynamics) + PFPL Cap 9
-    * 08/05: //paro//
-    * 13/05: **mini-control 2** + Coq demo
-    * 15/05: //paro//
-    * 20/05-22/05: //vacaciones//
-    * 27/05: PFPL Cap 16 (hasta 16.2)
-    * 29/05: PFPL Cap 16 y Cap 17 (intro)
-    * 03/06: PFPL Cap 17
-    * 05/06: TAPL Cap 13
-** Temas de presentación **
-====Type systems ====
-===security types ===
-Las políticas de flujo de información (information-flow policies) permiten clasificar entidades de un programa con distintos niveles de seguridad, para especificar confidencialidad o integridad.
-Los tipos de seguridad (security types) permiten enforzar information-flow policies de manera estática en tiempo de compilación.
-	* Programming Languages for Information Security
-		* http://www.cis.upenn.edu/~stevez/papers/Zda02.pdf
-		* Type rules, operational semantics, and noninterference
-		* Pure: pages 23-37
-		* Mutable references: 38-49
-===linear types===
-Los sistemas de tipos lineales pertenecen a la familia de sistemas de tipo subesctructurales donde una o más reglas estructurales están ausentes. En particular los sistemas de tipos lineales permiten "exchange", pero no "weakening" o "contraction". Esto quiere decir que cada variable de un programa debe ser usada exactamente una vez.
-Estos sistemas son generalmente usados para controlar recursos de sistema, como archivos, memoria o locks.
-	* Advanced Topics in Types and Programming Languages
-		* Substructural properties, type rules, operational semantics, progress + preservation.
-		* pages 3-16 (16-36: extensions and variations)
-===liquid types===
-Los liquid types permiten enriquecer tipos de un programa con predicados lógicos decidibles, los cuales permiten especificar y automatizar la verificación de propiedades semanticas de tu código. Un ejemplo característico del uso de estos tipos, es chequear estáticamente que no se produzcan divisiones por cero en un programa.
-	* http://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf
-===session types===
-Los session types son mayoritariamente usados en programación orientada a las comunicaciones, donde los programas pueden ser chequeados estáticamente para ver si respetan ciertos protocolos de comunicación.
-	* https://www.di.fc.ul.pt/~vv/papers/honda.vasconcelos.kubo_language-primitives.pdf
-	* Overview más gentil: http://www.di.unito.it/~dezani/papers/sto.pdf
-===dependent types===
-En lenguajes simples como el lambda cálculo simplemente tipado, se permite que términos dependan en variables (funciones).
-En lenguajes como System F, existe otro tipo de abstracción donde se permite que términos dependan ahora en tipos (abstracciones de tipo).
-Los lenguajes con tipos dependientes son lenguajes donde se permite ahora que los tipos dependan de términos del mismo lenguaje.
-    * Advanced Topics in Types and Programming Languages
-        * Dependant Types chapter
-        * pages 45 - 86
-    * Dependent ML: www.cs.bu.edu/fac/hwxi/academic/papers/JFPdml.ps
-    * Coq o F* (ver más abajo)
-===type and effects===
-Los sistemas de efectos permiten trackear los efectos secundarios que puede tener un programa, como por ejemplo imprimir en pantalla, leer y escribir en la memoria, tirar una excepción, etc.
-Los sistemas de tipos y efectos, como su nombre lo indica, combinan tipos y efectos para controlar de manera estática el uso de efectos en un programa.
-	* A Generic Type-and-Effect System: https://archive.alvb.in/msc/11_infomtpt/papers/generic-type-and-effect-system_Millstein.pdf
-===ownership types===
-Los tipos de pertenencia permiten clasificar objetos con una propiedad de pertenencia. Esto permite limitar la visibilidad de las referencias a los objetos, restringiendo el acceso fuera de su límites de encapsulación.
-Estos tipos son mayoritariamente empleados para manejo de alias, y eliminar data-races y deadlocks.
-	* https://www.cs.cornell.edu/courses/cs711/2005fa/papers/cpn-oopsla98.pdf
-	* http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.109.1645&rep=rep1&type=pdf
-===gradual types===
-Los tipos graduales permiten la suave transición entre el chequeo estático y el chequeo dinámico, basada en la precisión de las anotaciones de tipos introducidas por los programadores. Esto permite obtener los beneficios de lenguajes estáticamente tipados como Java, Scala, Haskell, y Ocaml, y lenguajes dinámicamente tipados como Javascript, Python, y Ruby.
-	* https://pdfs.semanticscholar.org/b7ca/4b0e6d3119aa341af73964dbe38d341061dd.pdf
-====Formal languages====
-===WebAssembly===
-WebAssembly es un lenguaje bytecode de bajo nivel y portable. Fue diseñado inicialmente para reemplazar Javascript en los navegadores web, pero ahora puede ser usado en cualquier otro contexto. WebAssembly está pensado para ser el posible objetivo de compilación de lenguajes de alto nivel  como C, C++ o Rust.
-	* Formal overview: https://dl.acm.org/citation.cfm?id=3062363
-===Rust===
-Rust es un lenguaje de programación de software de sistemas que se focaliza en "safety", especialmente para concurrencia segura. Rust es sintácticamente muy parecido a C++, pero esta designado con un rico sistema de tipos que permite un manejo seguro de la memoria y a la vez muy buen desempeño al no contar con un recolector de basura.
-	* https://www.rust-lang.org/
-	* https://plv.mpi-sws.org/rustbelt/popl18/paper.pdf
-===Scala===
-Scala es un lenguaje de programación que mezcla programación funcional con programación orientada a objetos. Tiene un sistema de tipos rico y su código fuente es compilado a bytecode para la JVM, lo que permite la interoperabilidad con cualquier libreria Java. Su uso conocido más popular es el de Twitter, los cuales cambiaron su infraestructura de Ruby a Scala.
-	* Formal: http://lampwww.epfl.ch/~odersky/papers/mfcs06.pdf
-	* Práctico: https://www.scala-lang.org/docu/files/ScalaOverview.pdf
-===F*===
-F* es un lenguaje de programación funcional con efectos, orientado a la verificación de programas. El sistema de tipos de F* incluye tipos dependientes, efectos monádicos, refinement types entre otros. F* permite la extracción de código a OCaml, F#, C, WASM o ASM. F* está siendo actualmente usado para implementar una versión verificada de todo el stack HTTPS (proyecto Everest), el cual incluye la implementación de TLS 1.2 y 1.3.
-	* https://fstar-lang.org/#papers
-===Coq===
-Coq es un lenguaje funcional con tipos dependientes y un demostrador de teoremas interactivo. Permite el ingreso de proposiciones matemáticas, las cuales son chequeadas mecánicamente, ayuda a construir demostraciones formales, y extrae programas certificados a lenguajes como OCaml, Haskell y Scheme.
-Aunque no es un demostrador de teoremas automático, incluye varias tácticas de demostraciones que ayudan en la construcción de ellas.
-	* https://coq.inria.fr/