Cómo aprender AGDA

Question

Estoy tratando de aprender AGDA.Sin embargo, tengo un problema.Todos los tutoriales que encontré en Agda Wiki son demasiado complejos para mí y cubren diferentes aspectos de la programación.Después de la lectura paralela de 3 tutoriales en Agda, pude escribir pruebas simples, pero todavía no tengo suficiente conocimiento para usarlo para la corrección de algoritmo de palabra real.

¿Puedes recomendarme algún tutorial sobre el tema?Algo similar a aprender a ti mismo un haskell, pero para Agda.

Answer 1

Cuando comencé a aprender AGDA hace aproximadamente un año, creo que probé todos los tutoriales disponibles y cada uno me enseñó algo nuevo.

Probablemente debe dar un intento de CoQ, porque tiene una base de usuarios más grande y hay dos libros agradables disponibles para él:

1. coq'art - ligeramente anticuado, pero para principiantes amigables
2. Programación certificada con tipos dependientes

   Software Foundations también es muy agradable.

   Lo bueno es que las teorías AGDA y COQ se basan en son algo similares, por lo que muchos ejemplos pueden traducirse de uno a otro. programación en la teoría de tipo de Martin-Löf es una introducción muy agradable y legible a la teoría de tipo dependiente , puede limpiar algunas cosas para ti.

   Ayudaría a saber qué quiere decir con "algoritmos del mundo real". Muchos desarrollos de ejemplo se describen en Papeles que mencionan AGDA .

Answer 2

Conor McBride le dio a una gran serie de conferencias el año pasado en la programación escritura de dependientes utilizandoAgda.Es un buen lugar para ir si quiere un descanso de verter los tutoriales de TERSE sobre el tema.Creo que también hay ejercicios de acompañamiento.