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:2019:presentaciones [2019/06/12 14:40] – etanterteaching:cc7110:2019:presentaciones [2019/06/12 14:49] (current) – etanter
Line 19: Line 19:
 Estos sistemas son generalmente usados para controlar recursos de sistema, como archivos, memoria o locks. 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+        * Linear Types Can Change the World: [[https://pdfs.semanticscholar.org/24c8/50390fba27fc6f3241cb34ce7bc6f3765627.pdf|pdf]]
  * Advanced Topics in Types and Programming Languages  * Advanced Topics in Types and Programming Languages
- * Substructural properties, type rules, operational semantics, progress + preservation. +            - Substructural properties, type rules, operational semantics, progress + preservation. 
- * pages 3-16 (16-36: extensions and variations)+            - pages 3-16 (16-36: extensions and variations)
  
  
Line 32: Line 32:
  * https://www.cs.cornell.edu/courses/cs711/2005fa/papers/cpn-oopsla98.pdf  * 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  * 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 (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, C++ o Rust.+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 +    * Formal overview: https://dl.acm.org/citation.cfm?id=3062363 
-        * homepage: https://webassembly.org/+    * homepage: https://webassembly.org/
  
  
Line 45: Line 56:
 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.
  
- * https://pdfs.semanticscholar.org/b7ca/4b0e6d3119aa341af73964dbe38d341061dd.pdf+    * 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]]
  
  
Line 67: Line 81:
  
  
-===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. 
- 
- * 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