Differences

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

--- teaching:cc7110:2019:presentaciones [2019/06/07 16:16] – mtoro
+++ teaching:cc7110:2019:presentaciones [2019/06/12 14:49] (current) – etanter
@@ Line 3: / Line 3: @@
 A continuación se muestra una lista de temas sugeridos para la presentación final del curso.
-* Esta lista es solo de referencia y están libres de escoger otro tema que propongan bajo acuerdo previo con el profesor
+Indicaciones:
-* Las presentaciones deben durar 20 minutos
+  * Esta lista es solo de referencia y están libres de escoger otro tema que propongan bajo acuerdo previo con el profesor
-* Las fechas de las presentaciones son Junio 24 y 26
+  * Los recursos que se listan a continuación de la descripción de cada tema también son de referencia. El objetivo de estos recursos es que sirvan como punto de partida
-* Cada presentación es individual
+  * Se espera que apliquen lo aprendido en el curso en sus presentaciones, por ejemplo mostrar reglas de tipo, reglas de reducción, etc
+  * Cada presentación es individual
+  * Las presentaciones deben durar máximo 20 minutos
+  * Las fechas de las presentaciones son Junio 24 y 26
+====== Temas seleccionados ======
+===Linear types (Daniela)===
+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.
+        * Linear Types Can Change the World: [[https://pdfs.semanticscholar.org/24c8/50390fba27fc6f3241cb34ce7bc6f3765627.pdf|pdf]]
+	* Advanced Topics in Types and Programming Languages
+            - Substructural properties, type rules, operational semantics, progress + preservation.
+            - pages 3-16 (16-36: extensions and variations)
+===Ownership types (Juan-Pablo)===
+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
+===Liquid types (Vicente)===
+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.
+	* Paper original de Liquid Types: http://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf
+	* Liquid Types en Haskell: https://goto.ucsd.edu/~nvazou/refinement_types_for_haskell.pdf
+	* Liquid Haskell in the Real World: http://goto.ucsd.edu/~nvazou/real_world_liquid.pdf
+===WebAssembly (Darío)===
+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 o Rust.
+    * Formal overview: https://dl.acm.org/citation.cfm?id=3062363
+    * homepage: https://webassembly.org/
+===Gradual types (Damian)===
+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.
+    * Paper original (Gradual Typing for FP): [[https://pdfs.semanticscholar.org/b7ca/4b0e6d3119aa341af73964dbe38d341061dd.pdf|pdf]]
+    * blog post de Siek: https://wphomes.soic.indiana.edu/jsiek/what-is-gradual-typing/
+    * Gradual Typing for Objects: [[https://www.researchgate.net/publication/225612648_Gradual_Typing_for_Objects|pdf]]
+    * Abstracting Gradual Typing: [[http://pleiad.dcc.uchile.cl/papers/2016/garciaAl-popl2016.pdf|pdf]]
+====== Otros temas propuestos ======
 ====Type systems ====
-===security types ===
+===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.
@@ Line 23: / Line 80: @@
-===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===
+===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.
@@ Line 47: / Line 90: @@
-===dependent types===
+===Dependent types===
 En lenguajes simples como el lambda cálculo simplemente tipado, se permite que términos dependan en variables (funciones).
@@ Line 60: / Line 103: @@
-===type and effects===
+===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.
@@ Line 67: / Line 110: @@
 	* 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===