Program in Coq

Programmation en Coq Dans cette thèse, nous cherchons à développer de nouvelles techniques pour écrire plus simplement des programmes formellement vérifiés. Nous procédons en étudiant l'utilisation de Coq en tant que langage de programmation dans différents environnements. Coq étant un langage purement fonctionnel, nous nous concentrons surtout sur la représentation et la spécification d'effets impurs, tel que les exceptions, les références mutables, les entrées-sorties et la concurrence.Nous travaillons premièrement sur deux projets préliminaires qui nous aident à comprendre les défis existants dans la programmation en Coq. Le premier projet, Cybele, est un plugin Coq pour écrire des preuves par réflexion efficaces avec effets. Nous compilons et nous exécutons les effets impurs en OCaml pour générer une prophétie, une forme de certificat, et interprétons les effets dans Coq en utilisant cette prophétie. Le second projet, le compilateur CoqOfOCaml, importe des programmes OCaml avec effets dans Coq en utilisant un système d'inférence d'effets.Puis nous décrivons différentes représentations génériques et composables d'effets impurs en Coq. Les calculs avec pause combinent les effets d'exceptions et de références mutables avec un mécanisme de pause. Ce mécanisme de pause permet de rendre explicite les étapes d'évaluation dans le but de représenter l'évaluation concurrente de deux termes. En implémentant le serveur web Pluto en Coq, nous réalisons que les entrées-sorties asynchrones sont l'effet le plus utile : cet effet est présent dans la plupart des programmes et ne peux être encodé de façon purement fonctionnelle. Nous concevons alors les "calculs asynchrones" comme moyen pour représenter et compiler des programmes avec événements en Coq.Finalement, nous étudions des techniques pour prouver des propriétés à propos de programmes avec effets. Nous commençons avec la vérification du système de blog ChickBlog écrit dans le langage des "calculs interactifs". Ce blog lance un fil d'exécution par client. Nous vérifions notre blog en utilisant une méthode de spécification par cas d'utilisation. Nous adaptons cette technique à la théorie des types en exprimant un cas d'utilisation comme un co-programme bien typé. Grâce à ce formalisme, nous pouvons présenter un cas d'utilisation comme un programme de test symbolique et le déboguer symboliquement, étape par étape, en utilisant le mode interactif de Coq. À notre connaissance, ceci représente la première telle adaptation de la spécification par cas d'utilisation en théorie des types. Nous pensons que la spécification formelle par cas d'utilisation est l'une des clés pour vérifier des programmes avec effets, sachant que la méthode des cas d'utilisation s'est avérée utile dans l'industrie pour exprimer des spécifications informelles. Nous étendons notre formalisme aux programmes concurrents et potentiellement non-terminants, avec le langage des "calculs concurrents". Nous concevons également un vérificateur de modèles pour vérifier l'absence d'interblocage dans un programme concurrent, en compilant la composition parallèle vers l'opérateur de choix non-déterministe.