Programación Certificada con Tipos Dependientes: Una Introducción Pragmática al Asistente de Pruebas Coq

Un manual sobre el software Coq para escribir y verificar pruebas matemáticas, con un enfoque práctico de ingeniería.

La tecnología de verificación mecanizada de programas puede desempeñar un papel de apoyo en muchos tipos de proyectos de investigación en ciencias de la computación, y las herramientas relacionadas para la verificación formal de pruebas están siendo cada vez más adoptadas en matemáticas e ingeniería. Este libro proporciona una introducción al software Coq para escribir y verificar pruebas matemáticas. Adopta un enfoque práctico de ingeniería en todo momento, haciendo hincapié en las técnicas que ayudarán a los usuarios a construir, comprender y mantener grandes desarrollos de Coq y a minimizar el costo del cambio de código con el tiempo.

Se cubren en detalle dos temas, rara vez discutidos en otros lugares: la programación dependientemente tipada eficaz (haciendo un uso productivo de una característica central del sistema Coq) y la construcción de tácticas de prueba específicas de dominio. Casi todos los temas cubiertos también son relevantes para la demostración interactiva de teoremas por computadora en general, no solo para la verificación de programas, demostrado a través de ejemplos de programas verificados aplicados en muchos tipos diferentes de formalizaciones. El libro desarrolla un estilo de prueba automatizado único y lo aplica en todo momento; incluso los usuarios experimentados de Coq pueden beneficiarse de leer sobre conceptos básicos de Coq desde esta nueva perspectiva. El libro también ofrece una biblioteca de tácticas, o programas que encuentran pruebas, diseñadas para usar con los ejemplos del libro. Los lectores adquirirán las habilidades necesarias para reimplementar estas tácticas en otros entornos al final del libro. Todo el código que aparece en el libro está disponible gratuitamente en línea.


Autor: Adam Chlipala
Editorial: MIT Press
Publicado: 07/06/2022
Páginas: 440
Tipo de encuadernación: Tapa blanda
Peso: 1.50lbs
Tamaño: 9.00h x 7.00w x 0.89d
ISBN13: 9780262545747
ISBN10: 0262545748
Categorías BISAC:
- Informática | Programación | General

Sobre el autor
Adam Chlipala es Profesor Asistente de Ingeniería Eléctrica y Ciencias de la Computación y Profesor de Desarrollo de Carrera Douglas T. Ross (1954) de Tecnología de Software en el MIT.