Bitácora

Programas Garantizados usando Tipos Dependientes

Ayer por la tarde el Grupo de Programación Funcional de Gotemburgo organizó una quedada para hablar de tipos dependientes. Como habitualmente, la plataforma de pagos Zimpler patrocinó las pizzas.

Vídeo y código fuente después del salto.

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.