BEGIN:VCALENDAR VERSION:2.0 PRODID:researchseminars.org CALSCALE:GREGORIAN X-WR-CALNAME:researchseminars.org BEGIN:VEVENT SUMMARY:Alberto Pardo (Universidad de la República\, Uruguay) DTSTART:20210429T170000Z DTEND:20210429T180000Z DTSTAMP:20260423T021030Z UID:LoReL/2 DESCRIPTION:Title: Fo rmalización de una transformación entre programas seguros usando un abor daje internalista\nby Alberto Pardo (Universidad de la República\, Ur uguay) as part of LoReL Seminar\n\n\nAbstract\nLos lenguajes funcionales f uertemente tipados\, como Haskell\, OCaml\, Agda o Idris\, entre otros\, s e destacan por sus sistemas de tipos. Gracias a sus poderosos mecanismos d e tipado (llamense tipos dependientes\, GADTs\, funciones a nivel de tipos \, múltiples kinds\, type classes\, etc) uno puede ir más allá del uso habitual que tienen los tipos en un lenguaje de programación y pasar a us arlos para para representar propiedades de los datos que manipula un progr ama (los llamados invariantes de tipos). Más allá del impacto (y dificul tad) que esto pueda implicar en la tarea de programación\, un benificio i mportante es que los invariantes pasan a formar parte del código ordinari o del programa y por lo tanto pueden ser verificados en tiempo de compilac ión por el chequeador de tipos del lenguaje. Es decir\, sólo son aceptad os aquellos programas que preservan los invariantes que tienen definidos e n sus tipos. Esta metodología de programación juega un rol clave\, por e jemplo\, en el desarrollo de software confiable. Al momento de codificar l os invariantes a nivel de los tipos existen distintas alternativas. Una es la estándar\, en la que uno asocia los invariantes a través de predicad os por fuera de la definición de los tipos. A este abordaje se le llama " externalista". Otra opción es usando un abordaje "internalista"\, en el q ue uno codifica el invariante como parte de la propia definición del tipo . De esta forma\, se chequea la propiedad en la propia construcción de lo s términos del tipo y por lo tanto sólo es posible construir aquellos t érminos que satisfacen el invariante. En esta charla analizaremos un ejem plo en particular donde aplicamos esta metodología de programación con i nvariantes. En concreto\, vamos a mostrar la formalización en Agda de una transformación entre programas seguros (de un lenguaje imperativo simple ) que preserva la propiedad de no interferencia. Dicha transformación tom a programas seguros según un sistema flow-sensitive (en el que el nivel d e seguridad de las variables puede mudar) y los transforma en programas se guros tipables según un sistema flow-insensitive (en el que el nivel de s eguridad de las variables es fijo). Lo interesante de nuestra formalizaci ón es que está desarrollada usando el abordaje internalista.\n LOCATION:https://researchseminars.org/talk/LoReL/2/ END:VEVENT END:VCALENDAR