El Centro Internacional Franco-Argentino de Ciencias de la Información y Sistemas (CIFASIS) será sede del primer encuentro del grupo de investigadores de Lenguajes de Programación "FunLeP".

FunLeP es un grupo de investigadores de la región (Argentina, Uruguay y Chile) que tiene por objetivo vincular investigadores en fundamentos de lenguajes de programación. Este es el primer encuentro, en el cual se presentarán cuatro charlas de diversos integrantes del grupo, y una reunión para decidir los pasos a seguir.

Se invita a investigadores y estudiantes de la región.

Organizador local: Mauro Jaskelioff

:: Programa

14:00hs Sesión 1

• • Hernán Melgratti (UBA): Tipos sesión y sus implementaciones

  • Federico Olmedo (UChile): Programas probabilísticos y su tiempo de ejecución

15:00hs Break

15:15hs Sesión 2

• • Beta Ziliani (UNC): Hacia la formalización del lenguaje Crystal

  • Alberto Pardo (UdelaR): An internalist approach to correct-by-construction compilers

16:15hs Coffee break

16:30hs Sesión 3

• • Debate sobre FunLeP. Moderador: Alejandro Díaz-Caro (ICC & UNQ)

Temario propuesto:

• • • Objetivos, Organización, Financiamiento

    • Encuentros: Frecuencia, estructura, invitados.

    • Lugar y fecha del próximo encuentro.

Detalles de las Charlas

Hernán Melgratti (UBA): Tipos sesión y sus implementaciones

Las sesiones se han establecido como un mecanismo clave para comunicar entre módulos en concurrentes programas.  Al igual que los valores entran o salen de una función u objeto, los mensajes se envían y se reciben desde un extremo de la sesión.  A diferencia de las funciones y objetos convencionales, el tipo, la dirección, y las propiedades de los mensajes intercambiados en una sesión pueden variar a medida que avanza la sesión.  Presentaremos los aspectos teóricos esenciales sobre los sistemas de tipo sesión y su implementación en lenguajes de programación.

Federico Olmedo (U. Chile): Programas probabilísticos y su tiempo de ejecución

Los programas probabilísticos son programas estándares que incluyen primitivas para realizar algún tipo de elección probabilística y resultan particularmente interesantes por su enorme campo de aplicación. Si bien dichos programas son típicamente simples, consistiendo en no más de 20 líneas de código, su comportamiento general, y en particular el análisis de su tiempo de ejecución, pueden volverse muy intrincados. En esta charla haremos una breve introducción a los programas probabilísticos y presentaremos una técnica para analizar su tiempo de ejecución de manera completamente formal.

Beta Ziliani (UNC): Hacia la formalización del lenguaje Crystal

El lenguaje de programación Crystal tiene muchos ingredientes que lo hacen atractivo. Éste hereda de Ruby su sintaxis y modelo de cómputo pero, a diferencia de éste, es tipado y compilado. Otro aspecto interesante es que los programas escritos en Crystal pueden en gran medida omitir su información de tipos, puesto que cuenta con un potente inferidor, permitiendo así transportar código de Ruby a Crystal casi sin cambios.

Desde el punto de vista formal, este lenguaje presenta varias aristas interesantes. Con un sistema de tipos complejo que mezcla tipos "unión" con conceptos de programación orientada a objetos, necesariamente el inferidor es incompleto, requiriendo eventuales anotaciones para guiarlo. Ahora, queda pendiente preguntas como: ¿El inferidor es correcto? ¿O será posible que éste infiera un tipo incorrecto en ciertas condiciones particulares no testeadas en la suite de test? En esta charla abordaré los trabajos que estamos realizando con el objetivo último de poder responder estas preguntas.

Alberto Pardo (UdelaR): An internalist approach to correct-by-construction compilers

One common approach in the design of a provable correct compiler is to write first the compiler, having in mind in that process the definitions of the syntax and semantics of the involved languages, and then, as a second step, to develop the correctness proof. This approach is known as externalist and has been investigated in several formal settings such as formal specification methods, categorical formalisations of programming languages, dependent types, etc. In this talk, we present on-going work on an alternative approach to formal compiler construction that follows an internalist discipline in which we develop simultaneously the compiler and its correctness proof. Our approach is based on the use of dependent types. The idea is to enrich the types of the abstract syntax trees of the languages with their own semantic values and then write the compiler as a function between those semantically enriched types where the correctness property is represented in the type of the function. As a result, that function plays the double role of compiler (i.e. AST translator) and proof term of the correctness property. In the talk we show the application of this approach to the translation between a simple while language and a semi-structured code for a stack machine. (This is a joint work with Emmanuel Gunther, Miguel Pagano and Marcos Viera).