Prof. Éric Tanter obtuvo un ACM SIGPLAN Distinguished Paper Award

Image preview

Prof. Éric Tanter.


Compartir

 

El profesor del DCC Éric Tanter obtuvo un nuevo reconocimiento, esta vez en la conferencia OOPSLA, donde obtuvo un ACM SIGPLAN Distinguished Paper Award.

 

“Gradual Liquid Type Inference”, se titula el paper del profesor Éric Tanter, realizado en conjunto con los investigadores de la Universidad de Maryland, David Van Horn y Niki Vazou, el cual obtuvo este año un ACM SIGPLAN Distinguished Paper Award, en la conferencia OOPSLA (Object-Oriented Programming, Systems, Languages & Applications) realizada en Boston, del 7 al 9 de noviembre 2018.

 

El profesor del DCC, destacó que el paper reconocido “demuestra cómo la noción de tipos refinados graduales (gradual refinement types) que desarrollamos junto con Nicolás Lehmann en su tesis de magíster (publicada en POPL’17) puede ser usada para asistir en la práctica para migrar código existente a que use tipos refinados. Además de la parte teórica, este paper demuestra este uso estudiando la migración de programas Haskell a Liquid Haskell (una extensión de Haskell con tipos refinados)”, explicó el profesor.

 

Cabe destacar que OOPSLA es una de las cuatro conferencias top de la ACM en el área de lenguajes de programación (junto con POPL, PLDI, ICFP), que abarca desde ingeniería de software con objetos, hasta teoría de lenguajes de programación, pasando por herramientas, análisis y validación, entre otros.

 

Resumen de “Gradual Liquid Type Inference”

 

Los tipos refinados representan una forma liviana de verificación de programas, enriqueciendo los tipos tradicionales con predicados lógicos. Los "tipos líquidos” es un mecanismo de inferencia decidable conveniente, pero que sufre de dos problemas mayores: (1) la inferencia es global y requiere anotaciones a nivel global, lo cual la hace inadecuada para inferencia modular de componentes, como librerías, (2) la inferencia produce mensajes de error oscuros. Ambos problemas afectan seriamente la migración de código existente para usar refinamientos.

 

Este artículo muestra que la inferencia de tipos líquidos graduales — una combinación novedosa de inferencia liquida y de tipos refinados graduales — soluciona ambos problemas. Los tipos refinados graduales, que soportan predicados imprecisos optimisticamente interpretados, pueden ser usados en posición de argumento para restringir la inferencia liquida para que la inferencia global infiera especificaciones efectivamente modulares para componentes de librerías. Desarrollamos la teoría de la inferencia de tipos líquidos graduales y exploramos su aplicación en el contexto de Liquid Haskell. Para demostrar la utilidad de nuestro enfoque, desarrollamos una herramienta interactiva, GuiLT, para inferencia de tipos líquidos graduales en Liquid Haskell que infiere tipos modulares y explora las concretizaciones seguras de refinamientos graduales. Aplicamos GuiLT al reporte de errores y analizamos un caso de estudio de la migración de tres librerías comunes de manipulación de listas en Haskell hacía Liquid Haskell.

 

--

 

Comunicaciones DCC