Ce cours couvre deux domaines complementaires : la programmation fonctionnelle en OCaml (Partie I) et les preuves formelles avec Coq (Partie II). Chaque partie compte 3 sessions de 2 heures.
Partie I — Programmation (OCaml)
Bases du langage
Lambda-calcul, codage de Church, syntaxe OCaml, calcul numerique (series, derivees, integrales).
Seance 2Traitements des donnees
Typage, listes, monades, dictionnaires, calcul vectoriel et descente de gradient.
Seance 3Arbres syntaxiques
AST, interpretation, transformation, calcul symbolique, mini compilateur et machine virtuelle.
Partie II — Preuves (CoqIDE)
Types et logique des propositions
Inference de types, correspondance de Curry-Howard, sequents, arbres de preuves.
Seance 5Logique des predicats
Quantificateurs, unification, raisonnement par induction, mini Prolog.
Seance 6Logique des Constructions
Types dependants, reecriture, verification de programmes (factorielle, listes, AST).
Travaux Pratiques
MusicFunk (OCaml)
Construire un langage de composition musicale : melodies, transformations, compilation ABC, visualisation ASCII.
TP2 — 4hMusicFunk (Coq)
Verifier formellement les proprietes de MusicFunk : retrograde involutif, transposition conserve les notes, etc.
Evaluation
ocaml.org • coq.inria.fr/doc • Software Foundations • abcnotation.com