Théorie de la programmation

Ce cours des L3 informatique fondamentale est assuré par Daniel Hirschkoff. Les TP et TD sont assurés par Antoine Plet, Alexandre Isoard et Jean-Marie Madiot. Ce sont pour l'instant des fichiers à trous à remplir avec le logiciel Coq.

• tp1.v : introduction à Coq : logique propositionnelle, égalité, arithmétique, prédicats, induction sur ℕ. (correction)
• tp2.v : sémantique à grands pas, prédicats inductifs, types de données inductifs (listes). (correction)
• tp3.v : induction sur prédicats inductifs, clôtures sur les relations, induction forte, déterminisme. (correction)
• td1.pdf : rédaction de preuves par induction, déterminisme, parallélisme (exemple de rédaction pour l'induction)
• tp4 : lex et yacc
• tp5.pdf : interprete miniML. Fichiers sources: miniml.tgz.
• td2.pdf : réécriture : terminaison, principe d'induction bien fondée, plongement dans ℕ
• td3.pdf : réécriture : terminaison, ordres lexicographique et multiensemble, confluence, faible normalisation.
• td4.pdf : réécriture : confluence (+ paires critiques), ordres de réduction (+ interprétations polynomiales).
• tp6.ml : algorithme d'unification.
• tp7.pdf : logique de Hoare, why3.