UP | HOME

Programmation certifiée avec Coq

Table of Contents

Ce cours s'adresse aux élèves de seconde année en apprentissage, recrutés après une formation initiale universitaire de deux ans consacrée à l'informatique. Le volume horaire est d'une quinzaine d'heures.

L'objectif du cours est l'apprentissage de la programmation certifiée,

Installation

Agenda - Liens vers les TP

  • 6 janvier - 1h15
    • Introduction
    • Les systèmes d'inférence
  • 9 janvier - 1h15
    • Les systèmes d'inférence (suite)
    • Logique
    • TP 1 + correction Tuto 1
  • 16 janvier - 1h15
    • Logique (suite) - Premier ordre, ordre supérieur
    • Correspondance de Curry-Howard
  • 24 janvier - 1h15
    • Systèmes d'inférence paramétrés et indexés
    • Du calcul des séquents aux tactiques
    • Exemple : les nombres binaires (TP2, Binaire.v dans le dépôt) - Style "preuve"
  • 27 janvier - 1h15
    • Exemple (suite) : les nombres binaires (TP2, Binaire.v dans le dépôt) - Style "preuve"
  • 30 janvier - 1h15
    • Tactiques liées à l'égalité et aux contradictions
    • Algèbres et systèmes d'inférence
      • Initialité
      • Quotient
    • Exemple : les nombres bianires (TP3, tp3.v dans le dépôt) - Style "preuve"
  • 3 février - 1h15
    • Algèbres et systèmes d'inférence (suite)
      • Initialité
      • Quotient
    • Exemple : les nombres bianires (TP3, tp3.v dans le dépôt) - Style "preuve"
  • 4 février - 1h15
    • Algèbres et systèmes d'inférence (suite et fin)
      • Initialité
      • Quotient
    • Exemple : les nombres bianires (TP3, tp3.v dans le dépôt) - Style "preuve"
  • 7 février - 2*1h15
    • Certification d'un tri par insertion
    • Extraction de code
  • 14 février - 2*1h15 - Evaluation

Introduction au cours - De l'efficacité surprenante de la logique en informatique

Les systèmes d'inférence

Logiques

De la logique aux tactiques

Types abstraits de données - Un point de vue algébrique

Coq : un guide

Software Foundations

Code à télécharger dans un même répertoire.

Evaluation

Author: Hervé Grall
Version history: latest: 2020-02-14.
Comments or questions: Send a mail.
The webpage content is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.