Introducción a la programación con tipos dependientes

El 1 de octubre de 2015 el Grupo de Programación Funcional de Gotemburgo organizó una quedada para hablar de tipos dependientes.

Vídeo de la charla (en inglés). Montado por Jean-Louis

Durante la sesión usamos Agda para jugar con tipos dependientes y entender su significado.

• Código fuente: Estos son los ejemplos que usé durante la presentación. Hay además muchas definiciones sin implementar, para que disfrutes resolviéndolas.

Damos las gracias a los chicos de Zimpler por patrocinar el picoteo.