Programación funcional verificada en Agda

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 propiedades de los programas a través de tipos ricos para los programas mismos. Esto a menudo requiere incluir pruebas dentro del código, para mostrar al verificador de tipos que las propiedades especificadas se cumplen. La capacidad de probar propiedades de los programas en estos dos estilos es una adición profunda 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 que era posible anteriormente. Programación funcional verificada en Agda es el primer libro en proporcionar una exposición sistemática de la verificación externa e interna en Agda, adecuado para estudiantes universitarios de Ciencias de la Computación. No se presupone familiaridad con la programación funcional ni con las pruebas verificadas por computadora. 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 los ejemplos de vectores, árboles de búsqueda binaria y árboles de Braun. También se incluye material más avanzado sobre computación a nivel de tipo, razonamiento explícito sobre la terminación y normalización por evaluación. El libro también incluye un estudio de caso de tamaño mediano sobre codificación y decodificación Huffman.

Autor: Aaron Stump
Editorial: ACM Books
Publicado: 01/02/2016
Páginas: 284
Tipo de encuadernación: Tapa blanda
Peso: 1.08lbs
Tamaño: 9.25h x 7.50w x 0.60d
ISBN13: 9781970001242
ISBN10: 1970001240
Categorías BISAC:
- Informática | Ciencias de la Computación
- Informática | Lenguajes | General

Sobre el autor
Aaron Stump es profesor de Ciencias de la Computación en la Universidad de Iowa. Sus intereses de investigación se centran en la Lógica Computacional y los Lenguajes de Programación, especialmente la Teoría de Tipos. Obtuvo una licenciatura en Ciencias de la Computación y Filosofía en la Universidad de Cornell en 1997, y un doctorado en Ciencias de la Computación en la Universidad de Stanford en 2002.