Séance de cours
Atelier Coq: Introduction au théorème interactif
Description
Cette séance de cours présente Coq, un assistant de théorème interactif basé sur l'isomorphisme de Curry-Howard. Il couvre les bases de la réalisation de preuves en Coq, définissant les types de données inductives, la sémantique opérationnelle et l'évaluation en plusieurs étapes. L’atelier vise à donner un aperçu des épreuves de Coq et de l’isomorphisme de Curry-Howard, en illustrant leurs applications.
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.