• el día 23 de Diciembre, se organizará un seminario donde todos tienen que participar.
• horarios:
  • Bloque 1 [10h-12h30]
    • Enzo: Rust (video)
    • José: Ownership Types
    • Andrés: Linear Types
    • Cristián: Liquid Types (slides)
    • Gaspar: Types and effects
  • almuerzo juntos con los que quieren
  • Bloque 2 [14h00-16h30]
    • Tomás V: Implicits 1 (slides)
    • Tomás D: Implicits 2
    • Stefano: Gradual Types (slides)
    • Francisco: Gradual Security Typing (slides)

• Cada presentación es individual
• Las presentaciones deben durar 15 minutos
  1. introducción (3 min)
  2. motivación (5 min): Demostración de la utilidad del sistema/lenguaje a través de un ejemplo
  3. desarrollo (6 min): Aspectos técnicos que justifican la sección anterior.
  4. conclusiones (1 min).

• se considerará su presentación (50%), manejo de las preguntas (25%), y su participación general en el workshop (25%)

A continuación se muestra una lista de temas sugeridos para la presentación final del curso.

Indicaciones:

• Esta lista es solo de referencia y son libres de escoger otro tema que propongan bajo acuerdo previo Éric y Stefan
• 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
• Se espera que apliquen lo aprendido en el curso en sus presentaciones, por ejemplo mostrar reglas de tipo, reglas de reducción, enunciados formales de propiedades, etc

Les recordamos que pueden proponer cualquier tema que les parezca interesante (con un (par de) paper(s) de referencia). Por ejemplo, en clase surgió esto de Non-parametric parametricity. Siéntanse libres de explorar y conversarlo con nosotros!

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: pdf
• Advanced Topics in Types and Programming Languages
  1. Substructural properties, type rules, operational semantics, progress + preservation.
  2. pages 3-16 (16-36: extensions and variations)

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

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

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): pdf
• blog post de Siek: https://wphomes.soic.indiana.edu/jsiek/what-is-gradual-typing/
• Gradual Typing for Objects: pdf
• Refined criteria for gradual typing: pdf
• Abstracting Gradual Typing: pdf

Además, se puede aplicar las ideas de gradual typing a distintos sistemas de tipos, p.ej:

• Gradual refinement types: pdf
• Gradual effects: pdf
• Gradual security typing (Pancho): pdf

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: pdf

Algunos lenguajes (como 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
• Simplicitly: Foundations and Applications of Implicit Function Types: https://dl.acm.org/doi/pdf/10.1145/3158130

Definir una familia de programas con alguna(s) variacion(es) es algo muy común en el desarrollo de software. Es posible diseñar un lenguaje con un soporte explicito para variaciones, que simplifica muchos aspectos, tanto de implementación como de

• The Choice Calculus: A Representation for Software Variation: https://dl.acm.org/doi/10.1145/2063239.2063245
• A calculus for variational programming: pdf

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

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/

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 librería Java. Muchos aspectos de Scala fueron estudiados formalmente y publicados. Hay muchos temas de presentación posibles en torno a Scala, aquí va una selección no-exhaustiva:

• General ideas of the unification of OOP and FP: https://doi.org/10.1145/2591013
• Generics of a higher kind: https://doi.org/10.1145/1449764.1449798
• Pattern matching for objects: https://doi.org/10.1007/978-3-540-73589-2_14
• Foundations of path-dependent types: https://doi.org/10.1145/2660193.2660216
• Core calculus de Scala 3 (dependent object types): https://doi.org/10.1007/978-3-319-30936-1_14
• Foundations of implicit function types: https://doi.org/10.1145/3158130
• Type classes as objects and implicits: https://doi.org/10.1145/1869459.1869489
• Safer exceptions for Scala: https://dl.acm.org/doi/10.1145/3486610.3486893
• (ver también el punto sobre implicit parameters más arriba)

Idris es un lenguaje funcional de propósito general con tipos dependientes. Idris está diseñado para favorecer el *desarrollo impulsado por tipos* (type-driven development). En el desarrollo impulsado por tipos, los tipos son una herramienta para construir programas: los tipos describen una especificación y el typechecker ayuda al desarrollador a seguirla.

• https://www.idris-lang.org
• Idris, a General Purpose Dependently Typed Programming Language: Design and Implementation: https://doi.org/10.1017/S095679681300018X
• Idris 2: Quantitative Type Theory in Practice: pdf

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