Una excelente noticia para nuestro DCC fue el reconocimiento “Distinguished Paper Award” que recibieron el Profesor Éric Tanter y los alumnos de Doctorado en Computación, Elizabeth Labrada y Matías Toro, por su trabajo de investigación “Gradual Parametricity, Revisited”. La distinción fue otorgada en el marco de la Conferencia POPL 2019 (Principles of Programming Languages), la más antigua y prestigiosa del área de lenguajes de programación, que se realizó del 13 al 19 de enero en Portugal.

Este premio destaca los trabajos que, a juicio del comité de programa de la conferencia, deben ser leídos por una amplia audiencia debido a su relevancia, originalidad, importancia y claridad. El Profesor Éric Tanter explicó que el paper “resuelve un problema de largo aliento en el área de lenguajes con tipos graduales, el cual lleva más de 10 años siendo estudiado por varios investigadores. Explica cómo diseñar un lenguaje gradual que soporte “parametricidad”, es decir, la uniformidad de comportamiento de las expresiones con tipos polimórficos”, afirmó.

Resumen “Gradual Parametricity, Revisited”

Brindar los beneficios del tipado gradual a un lenguaje con polimorfismo paramétrico como System F, preservando parametricidad relacional, ha demostrado ser extremadamente difícil de lograr: los primeros intentos fueron formulados hace diez años, y varios diseños fueron propuestos recientemente. Entre otros problemas, estas propuestas pueden señalar errores de parametricidad en situaciones inesperadas, y no manejan adecuadamente las instanciaciones de tipos con tipos imprecisos. Estas observaciones sugieren que los cálculos de casts existentes no son adecuados para soportar una versión gradual de System F.

En este trabajo, revisitamos el desafío de diseñar un lenguaje gradual con polimorfismo paramétrico explícito, explorando en qué medida la metodología de Abstracting Gradual Typing nos ayuda a derivar este lenguaje, GSF. Presentamos el diseño y la metateoría de GSF, y proveemos una implementación de referencia. Además de evitar los problemas de semántica identificados, GSF satisface las propiedades de un lenguaje gradual paramétrico, salvo una: la garantía gradual dinámica, que fue dejada como conjetura en trabajos anteriores, es aquí mostrada como incompatible con parametricidad. Sin embargo, establecemos una propiedad más débil que nos permite aclarar el tipo de razonamiento que soporta la parametricidad gradual.

--
Comunicaciones DCC