Programmation en Coq

Les documents accessibles depuis cette page sont les premières versions de plusieurs chapitres d'un livre en cours de rédaction sur l'utilisation de Coq pour décrire des programmes et raisonner sur ces programmes. Les aspects suivants sont couverts:

Les types inductifs en Coq

des types de données récursifs aux propriétés inductives, descriptions des principes de récurrence et de la preuve par récurrence.

Fonctions en Coq

Méthodes pour décrire des fonctions récursives et prouver des propriétés de ces fonctions

Tri par insertion

Description de l'algorithme de tri par insertion, en commençant par les descriptions abstraites et en poussant l'étude jusqu'à une implémentation impérative de l'algorithme.