Programación Funcional Verificada en Agda

Opiniones de los lectores

El libro es elogiado como una introducción accesible a los tipos dependientes utilizando Agda, en particular para la demostración práctica de teoremas. Sin embargo, tiene notables defectos de claridad, organización y presentación, lo que afecta a su eficacia general.

La introducción más accesible a los tipos dependientes en la práctica, especialmente para Agda.

Prepara a los lectores para libros más avanzados sobre el tema.

(basado en 4 opiniones de lectores)

Título original:

Verified Functional Programming in Agda

Contenido del libro:

Agda es un lenguaje de programación avanzado basado en la Teoría de Tipos. El sistema de tipos de Agda es lo suficientemente expresivo como para soportar la verificación funcional completa de programas, en dos estilos.

En la verificación externa, escribimos programas funcionales puros y luego escribimos pruebas de propiedades sobre ellos. Las pruebas son artefactos externos separados, típicamente usando inducción estructural. En la verificación interna, especificamos las propiedades de los programas a través de tipos ricos para los propios programas.

Esto a menudo requiere incluir pruebas dentro del código, para mostrar al verificador de tipos que las propiedades especificadas se mantienen. El poder de demostrar las propiedades de los programas en estos dos estilos es una profunda adición a la práctica de la programación, dando a los programadores el poder de garantizar la ausencia de errores, y por lo tanto mejorar la calidad del software más de lo posible anteriormente. Verified Functional Programming in Agda es el primer libro que proporciona una exposición sistemática de la verificación externa e interna en Agda, adecuada para estudiantes universitarios de Informática.

No se presupone ninguna familiaridad con la programación funcional ni con las pruebas verificadas por ordenador. El libro comienza con una introducción a la programación funcional a través de ejemplos familiares como booleanos, números naturales y listas, y técnicas para la verificación externa. La verificación interna se considera a través de ejemplos de vectores, árboles de búsqueda binarios y árboles de Braun.

También se incluye material más avanzado sobre computación a nivel de tipo, razonamiento explícito sobre terminación y normalización por evaluación. El libro también incluye un caso práctico de tamaño medio sobre la codificación y descodificación Huffman.