Differences

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

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision		Previous revision
teaching:cc7110:2021:presentaciones [2021/11/23 14:29] – [CC7110 - Workshop Final] smalewskiteaching:cc7110:2021:presentaciones [2021/12/23 15:26] (current) – [CC7110 - Workshop Final] smalewski
Line 1: Line 1:
 ====== CC7110 - Workshop Final  ====== ====== CC7110 - Workshop Final  ======
 +
  
 ===Workshop=== ===Workshop===
   * el día 23 de Diciembre, se organizará un seminario donde todos tienen que participar.    * el día 23 de Diciembre, se organizará un seminario donde todos tienen que participar. 
   * horarios:    * horarios: 
-      * Bloque 1: 10h-12h30 +      * Bloque 1 [10h-12h30]  
 +        * Enzo: Rust ([[https://drive.google.com/file/d/144_uDbXPxJPnQLogY7S5ZiI2oWFUzXDQ/view?usp=drive_web|video]]) 
 +        * José: Ownership Types  
 +        * Andrés: Linear Types  
 +        * Cristián: Liquid Types ([[https://drive.google.com/file/d/1uFlfgIG2Hp52sFsOx6BKjAOnW0kyK-AP/view?usp=sharing|slides]]) 
 +        * Gaspar: Types and effects
       * almuerzo juntos con los que quieren       * almuerzo juntos con los que quieren
-      * Bloque 2: 14h00-16h30+      * Bloque 2 [14h00-16h30]  
 +        * Tomás V: Implicits 1 ([[https://docs.google.com/presentation/d/17llqaj5WkTHA15CWpULB7elJwDgCjqXk/edit?usp=sharing&ouid=100382086267036499345&rtpof=true&sd=true|slides]]) 
 +        * Tomás D: Implicits 2  
 +        * Stefano: Gradual Types ([[https://drive.google.com/file/d/1V05KF6RC5c2u-xn1Y3jHYQ1RT80tQzmw/view?usp=sharing|slides]]) 
 +        * Francisco: Gradual Security Typing ([[https://drive.google.com/file/d/1ujFNc8O8N7hKnHC5P2DEIyZiA5ByMPX6/view?usp=sharing|slides]]) 
  
 ===Presentaciones=== ===Presentaciones===
Line 18: Line 29:
 ===Evaluación=== ===Evaluación===
   * se considerará su presentación (50%), manejo de las preguntas (25%), y su participación general en el workshop (25%)   * se considerará su presentación (50%), manejo de las preguntas (25%), y su participación general en el workshop (25%)
- 
  
 ---- ----
Line 36: Line 46:
  
  
-===Linear types===+===Linear types (Andrés)===
   
 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.  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. 
Line 47: Line 57:
  
  
-===Ownership types===+===Ownership types (José)===
  
 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. 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.
Line 57: Line 67:
  
  
-===Liquid types===+===Liquid types (Cristian)===
   
 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. 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.
Line 67: Line 77:
  
  
-===Gradual types===+===Gradual types (Stefano)===
  
 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.  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. 
Line 80: Line 90:
     * Gradual refinement types: [[http://pleiad.dcc.uchile.cl/papers/2017/lehmannTanter-popl2017.pdf|pdf]]     * Gradual refinement types: [[http://pleiad.dcc.uchile.cl/papers/2017/lehmannTanter-popl2017.pdf|pdf]]
     * Gradual effects: [[http://pleiad.dcc.uchile.cl/papers/2014/banadosAl-icfp2014.pdf|pdf]]     * Gradual effects: [[http://pleiad.dcc.uchile.cl/papers/2014/banadosAl-icfp2014.pdf|pdf]]
-    * Gradual security typing: [[http://pleiad.dcc.uchile.cl/papers/2018/toroAl-toplas2018.pdf|pdf]]+    * Gradual security typing (Pancho): [[http://pleiad.dcc.uchile.cl/papers/2018/toroAl-toplas2018.pdf|pdf]]
  
  
-===Type and effects===+===Type and effects (Gaspar: Excepciones)===
   
 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 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.
Line 90: Line 100:
  * A Generic Type-and-Effect System: [[https://archive.alvb.in/msc/11_infomtpt/papers/generic-type-and-effect-system_Millstein.pdf|pdf]]  * A Generic Type-and-Effect System: [[https://archive.alvb.in/msc/11_infomtpt/papers/generic-type-and-effect-system_Millstein.pdf|pdf]]
  
-===Implicits===+===Implicits (Tomás D. en Coq y Tomás V. en Scala)===
  
 Algunos lenguajes (como [[https://docs.scala-lang.org/tour/implicit-parameters.html|Scala]]) soportan parámetros implícitos, un mecanismo para programación genérica que permite la inferencia de ciertos términos en base a información de tipo. Un mecanismo similar se encuentra en Coq, donde uno puede omitir ciertos argumentos y dejar que Coq los infiera. Los implicits son en esencia una generalización de las type classes (introducidas en Haskell). Algunos lenguajes (como [[https://docs.scala-lang.org/tour/implicit-parameters.html|Scala]]) soportan parámetros implícitos, un mecanismo para programación genérica que permite la inferencia de ciertos términos en base a información de tipo. Un mecanismo similar se encuentra en Coq, donde uno puede omitir ciertos argumentos y dejar que Coq los infiera. Los implicits son en esencia una generalización de las type classes (introducidas en Haskell).
  
     * The implicit calculus: a new foundation for generic programming: https://dl.acm.org/doi/10.1145/2345156.2254070     * The implicit calculus: a new foundation for generic programming: https://dl.acm.org/doi/10.1145/2345156.2254070
 +    * Simplicitly: Foundations and Applications of Implicit Function Types: https://dl.acm.org/doi/pdf/10.1145/3158130
  
 ===Variational programming=== ===Variational programming===
Line 109: Line 120:
  
  
-===Rust===+===Rust (Enzo)===
   
 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. 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.