Mini-curso de Programación con Tipos dependientes
Los tipos dependientes permiten unificar la programación y la verificación de programas ya que los tipos pueden ser lo suficientemente precisos como para expresar una especificación. En este curso, veremos una introducción práctica a las características básicas de la programación con tipos dependientes usando el lenguaje funcional Agda y su entorno interactivo de desarrollo. Para ello, implementaremos algunos ejemplos simples pero interesantes.
Día 1
Bajar el archivo IntroEj.agda y cargarlo con Emacs. Completar todos los agujeros.
Día 2
Un pequeño compilador.
Bajar el archivo Outro.agda y extender el lenguaje con pares.