Fearless Programming and Reasoning with Infinities

En nuestro próximo evento, contaremos con Alex Gryzlov del IMDEA Software, en el que veremos cómo formalizar la noción de infinito en nuestros programas (streams, sistemas operativos, etc.) utilizando Agda como vehículo. Se trata de una charla presencial y en inglés.

¡¡¡MUY IMPORTANTE!!! Es obligatorio rellenar este formulario (nombre, apellidos e identificación) para poder acceder al Madrid International Lab. En ningún caso se utilizará esta información para fines comerciales y será eliminada una vez tenga lugar el evento.

Abstract & Bio

Typed functional programming emphasizes separating effects and logical constructs to simplify formal and informal reasoning about program behavior and correctness. However, type-based reasoning usually overlooks a fundamental kind of effect: one of non-termination. This can make it hard to distinguish between endlessly looping behavior introduced by mistake and one deliberately designed to be infinite. Cyclic but useful programs are ubiquitous in everyday programming - think of device drivers, operating systems, runtime environments, web servers, and data stream processing services. In this talk, we will use the Agda theorem prover augmented with a type-theoretic mechanism for manipulating thunks to explore the world of formalized lazy algorithms and infinite data structures such as streams, automata, and coroutines.

Alex Gryzlov is a research software engineer at the IMDEA Software Institute in Madrid, working on the LiquidHaskell verification tool and its theory. Before doing formal methods, he worked in various programming fields like back-end development, bioinformatics, and data engineering.