¿Cómo haría para aprender la teoría subyacente del asistente de prueba Coq?

Respuestas:

32

Un lugar para comenzar es el manual de referencia de Coq ( pdf ). El Capítulo 4 describe la lógica subyacente de Coq y, en última instancia, todo se basa en esto. Se llama el cálculo de las construcciones (co) inductivas, y muchos documentos lo describen. Tener en sus manos el libro Coq'Art Interactive Theorem Proving and Program Development ofrece una introducción más relajada pero no barata a Coq.

Para conocer cómo funcionan las tácticas, eche un vistazo a esta pregunta anterior: ¿Cómo funcionan las 'tácticas' en asistentes de prueba?

Para desarrollar la teoría requerida, debe aprender sobre la teoría de tipos . Lo más relacionado con la teoría subyacente a un asistente de prueba es probablemente las notas (o libro ) de la teoría de tipo intuitiva de Per Martin-Löf o el libro Programación en la teoría de tipo de Martin-Löf , que realmente trata sobre escribir y probar teoremas en la teoría de tipos. Se puede obtener una perspectiva del lenguaje de programación sobre la teoría de tipos en los Tipos y Lenguajes de Programación de Pierce . Las pruebas y tipos de Girard et al , que también abordan la importancia de la correspondencia Curry-Howard , es otra excelente referencia. Entonces probablemente estés bien y verdaderamente listo para leer Coquand y HuetEl cálculo de las construcciones . Finalmente, busque algunas de las referencias en la parte posterior del manual de Coq.

Hay otros asistentes de pruebas , HOL, NuPRL, Mizar, Twelf, etc., y también tienen su teoría, por lo que también puedes aprender mucho leyendo en esa dirección.

Finalmente, para obtener una descripción general de la historia y el futuro de los asistentes de pruebas, consulte el reciente artículo de Herman Geuvers.

Dave Clarke
fuente
55
Buena lista Agregaré un orden de lectura. TAPL de Pierce cubre el fondo; la mayoría del resto no tendrá sentido hasta que domines las reglas de escritura. El Capítulo 2 de ATTAPL introduce los tipos dependientes con relativa suavidad. Luego, puede leer el capítulo 4 del manual de Coq, que tiene las reglas de escritura (debe verificar la bibliografía para obtener información avanzada, como las reglas exactas para la recursividad). Paralelamente, el libro Coq'Art tiene una perspectiva más práctica. Consejo extra: Show Treeen coq.
Gilles 'SO- deja de ser malvado'
2
Soy alguien en más o menos la misma posición que el OP aunque un poco más adelante. Después de experimentar un poco, finalmente encontré el orden 1) Aprender programación funcional 2) leer TAPL 3) Leer sobre tipos dependientes en ATTAPL para trabajar mejor que otras cosas. Me alegra saber que estoy aproximadamente en el camino correcto.
John Salvatier
1
Yo también estuve aquí y obtuve el libro Coq'Art. Es absolutamente perfecto para la comprensión, entran en cada táctica en detalle y explican cuándo y cómo usarlo. El libro también lo guía rápidamente a través de cada regla básica en teoría de tipos, enseñándole notación y cómo usarlo en Coq. Me encanta este libro.
Lance Pollard
6

El libro de Luo sobre el cálculo extendido de construcciones también es una buena referencia. ECC fue bastante influyente en el diseño de la teoría de tipos de Coq.

Dominic Mulligan
fuente