Comment pourrais-je apprendre la théorie sous-jacente de l'assistant de preuve Coq?

Réponses:

32

Le manuel de référence du Coq ( pdf ) constitue un bon point de départ. Le chapitre 4 décrit la logique sous-jacente de Coq et, finalement, tout est basé sur celle-ci. C'est ce qu'on appelle le calcul des constructions (co) inductives, et de nombreux articles le décrivent. Mettre la main sur le livre de Coq'Art Le test de théorème interactif et le développement de programmes fournit une introduction plus tranquille mais pas moins chère à Coq.

Pour en savoir plus sur le fonctionnement des tactiques, jetez un œil à la question précédente: comment les «tactiques» fonctionnent-elles dans les assistants de preuve?

Pour construire la théorie requise, vous devez vous familiariser avec la théorie des types . Le plus étroitement lié à la théorie sous-jacente à un assistant de preuve est probablement les notes (ou livre ) sur la théorie des types d'Intuitionnisme de Per Martin-Löf ou le livre Programmation dans la Théorie des types de Martin-Löf , qui concerne en réalité l'écriture et la démonstration de théorèmes dans la théorie des types. Une perspective du langage de programmation sur la théorie des types peut être obtenue à partir des types et langages de programmation de Pierce . Les preuves et types de Girard et al , qui aborde également l’importance de la correspondance Curry-Howard , constituent une autre excellente référence. Alors vous êtes probablement bel et bien prêt à lire celui de Coquand et HuetLe calcul des constructions . Enfin, cherchez quelques-unes des références à la fin du manuel Coq.

Il existe d'autres assistants de preuve , HOL, NuPRL, Mizar, Twelf, etc., et ils ont également leur théorie. Vous pouvez donc en apprendre beaucoup également en lisant dans ce sens.

Enfin, pour un aperçu de l’histoire et de l’avenir des assistants de preuve, consultez le récent article de Herman Geuvers.

Dave Clarke
la source
5
Belle liste. Je vais ajouter un ordre de lecture. Le TAPL de Pierce couvre le fond; la plupart des autres n'auront aucun sens tant que vous ne maîtriserez pas bien les règles de dactylographie. Le chapitre 2 de ATTAPL présente les types dépendants de manière relativement douce. Ensuite, vous pouvez lire le chapitre 4 du manuel Coq, qui contient les règles de dactylographie (vous devez consulter la bibliographie pour des informations plus avancées, telles que les règles exactes pour la récursion). En parallèle, le livre Coq'Art présente une perspective plus pratique. Bonus: Show Treeen coq.
Gilles 'SO- arrête d'être méchant'
2
Je suis quelqu'un qui se trouve à peu près dans la même position que le PO, mais un peu plus loin. Après quelques expériences, j'ai finalement trouvé l'ordre 1) Apprendre la programmation fonctionnelle 2) Lire TAPL 3) Lire des informations sur les types dépendants dans ATTAPL pour qu'ils fonctionnent mieux que d'autres. Heureux de savoir que je suis à peu près sur le bon chemin.
John Salvatier
1
J'étais là aussi et j'ai reçu le livre Coq'Art. Il est absolument parfait pour comprendre. Ils décrivent chaque tactique en détail et expliquent quand et comment l’utiliser. Le livre vous guide également rapidement dans toutes les règles de base de la théorie des types, vous expliquant la notation et son utilisation en Coq. Aimer ce livre.
Lance Pollard
15

En ce qui concerne le calcul lambda typé, la logique intuitionniste, divers systèmes de preuves et l'isomorphisme de Curry-Howard, qui font tous partie du contexte mathématique de Coq, je recommande fortement "Conférences sur l'isomorphisme de Curry-Howard" (de P. Urzyczyn et M. Sørensen).

Marcin Kotowski
la source
Nous semblons être sur la même longueur d'onde aujourd'hui. ;-)
Marc Hamann
Cela semble être le jour de Curry-Howard: cstheory.stackexchange.com/questions/5848/…
Dave Clarke le
6

Le livre de Luo sur le calcul étendu des constructions est également une bonne référence. ECC a eu une influence considérable sur la conception de la théorie des types de Coq.

Dominic Mulligan
la source