A Very Formal Evening

Nos alegra anunciaros un nuevo evento en FP Madrid. En esta ocasión contaremos con Niki Vazou (IMDEA Software), Juanjo Madrigal y Jorge Luis Mayoral (Devo). Será una tarde "muy formal" con dos charlas (la primera en inglés y la segunda en español) donde los tipos refinados y los tipos dependientes serán los protagonistas.

Nos gustaría agradecer enormemente a Idealista por cedernos sus magníficas instalaciones para celebrar este evento.

Agenda
18:15 Registration
18:30 Niki Vazou (IMDEA Software) Liquid Haskell: Verification with Refinement Types.
19:15 Juanjo Madrigal y Jorge Luis Mayoral (Devo) El Señor de los Sistemas de Tipos.
20:00 Networking

Speakers & Abstracts

Niki Vazou (IMDEA Software) Liquid Haskell: Verification with Refinement Types. Refinement types decorate the types of a programming language with logical predicates to allow more expressive type specifications. Originally, refinement type based specifications were restricted to SMT decidable theories and allowed automatic “light” verification, for example properties like non-division by zero or in-bound indexing. Verification of such light properties though requires “deeper” specifications, for example “is append associative?” In this talk, we will interactively see how to use the refinement type checker of Liquid Haskell to verify Haskell programs.

Niki is an Associate Research Professor at IMDEA Software Institute. She received her Ph.D. at UC San Diego, where she co develop Liquid Haskell, a refinement type checker for Haskell programs. Since then, she works on both the theory of refinement typing and their applications to verify real world properties. For this research purpose, in 2022 she received the ERC Starting Grant CRETE.

Juanjo Madrigal y Jorge Luis Mayoral (Devo) El Señor de los Sistemas de Tipos. Todo comenzó con la forja de los Sistemas de tipos...
Unos permitían trabajar con tipos primitivos como int, char...
Otros, sofisticados, permitían trabajar con listas, optional...
En estos sistemas residía el poder de expresión que conocemos
en nuestros lenguajes del día a día...
Pero todos ellos fueron engañados, pues otro sistema más
fue forjado: el Sistema de Tipos Dependientes. En este sistema
reside el poder y la expresividad no solo de todos los demás,
sino de instaurar la Lógica dentro de sí mismo...

Juanjo Madrigal is half mathematician and half programmer; he moved from pure maths (geometry and topology, and other weird stuff) to languages and types and compilers (more weird stuff XD) and he loves both, especially when they mix. He's currently a software engineer at Devo, working in the interactive search and the query engines, where he always finds challenging problems worth solving.

Jorge is a software developer who comes from the world of pure mathematics: geometry and topology. Although he loves programming, he has never been able to overcome his mathematical roots, always trying to find some bit of mathematical formalism in the software language. In his free time he is a level 8 Sorcerer with a lot of charisma. Nowadays he enjoys developing query models at Devo, where every day is a challenge on a theoretical and practical level.