La Conferencia Internacional en Programación Funcional, ICFP 2019 (International Conference on Functional Programming) aceptó tres artículos de investigación del profesor del DCC e investigador del Instituto Milenio Fundamentos de los Datos (IMFD), Éric Tanter.

Se trata de los trabajos, “Approximate Normalization for Gradual Dependent Types”, sobre sistemas de tipos; “A Reasonably Exceptional Type Theory”, acerca de teoría de tipos; y “Dijkstra Monads for All”, sobre verificación de programas; que serán presentados en una de las más prestigiosas conferencias sobre lenguajes de programación en el mundo.

Acerca del primer artículo, el profesor Tanter explicó que la idea surgió de una colaboración con el estudiante de doctorado de la Universidad de Columbia Británica (UBC), en Canadá, Joseph Eremondi, y su profesor guía de doctorado y académico de la UBC, Ronald Garcia.

“Desde hacía un tiempo tenía la idea de trabajar en torno a una versión gradual de sistemas de tipos dependientes”, precisó el académico. “Los tipos dependientes sirven para desarrollar sistemas con muy fuertes garantías de confiabilidad. No obstante, su adopción es difícil por causa del nivel de complejidad que presentan, por lo cual formulamos una propuesta de chequeo gradual de tipos para resolver la integración y la transición entre sistemas con y sin tipos”, agregó.

Al referirse a los artículos “A Reasonably Exceptional Type Theory” y “Dijkstra Monads for All”, el profesor Tanter sostuvo que, mientras el primero plantea una mejora a una propuesta previa de los investigadores del Instituto Nacional de Investigación en Ciencias Digitales de Francia (INRIA) Nicolas Tabareau y Pierre-Marie Pédrot; el segundo presenta nuevos fundamentos para la verificación de programas con efectos secundarios modelados como mónadas o estructuras que representan cálculos como una secuencia de pasos.

“En el trabajo, ‘A Reasonably Exceptional Type Theory’, planteamos la posibilidad de razonar de manera consistente en torno a programas computacionales del mundo real, capaces de expresar excepciones o indicaciones de error, desde el punto de vista lógico”, dijo el profesor Tanter.

La propuesta, coescrita con los investigadores, Pierre-Marie Pédrot (INRIA), Nicolas Tabareau (INRIA) y Hans Fehrmann (DCC UChile), aborda de una manera flexible el dilema entre excepción y consistencia y, además, propone un complemento para el sistema de gestión de pruebas para lenguajes formales Coq.

En cuanto a “Dijkstra Monads for All”, el profesor del DCC e investigador del IMFD mencionó que presenta nuevos fundamentos para la verificación de programas con efectos monádicos.

“Las mónadas de Dijkstra ya se usan en el lenguaje de programación y verificación F*, desarrollado por Microsoft Research y la idea central de esta investigación es que, de cada efecto especificado como una mónada, uno puede derivar una mónada para verificar programas que usan dicho efecto. La contribución es bien teórica, incluyendo algo de teoría de categorías, pero su impacto en la práctica puede ser considerable, ya que va a permitir más flexibilidad en la verificación automática de programas”, especificó el profesor Éric Tanter.

“Dijkstra Monads for All” fue coescrito por el profesor Tanter junto a los investigadores, Kenji Maillard (Inria, París; Escuela Normal Superior de París), Danel Ahman (Universidad de Liubliana, Eslovenia), Robert Atkey (Universidad de Strathclyde, Escocia), Guido Martínez (CIFASIS-CONICET, Argentina), Cătălin Hriţcu (Inria, París), Exequiel Rivas (Inria, París).

La presentación de los trabajos, “Approximate Normalization for Gradual Dependent Types”, “A Reasonably Exceptional Type Theory” y “Dijkstra Monads for All”, tendrá lugar en la sección de artículos de investigación de la conferencia, ACM SIGPLAN ICFP, que se realizará entre el 19 y 21 de agosto en Berlín, Alemania.