Logique, déduction et programmation

Page web du Master 1 Informatique 2005 au CMI.

Nouveautés

• Les notes de l'examen.
• Corrigé de l'examen.
• Date limite pur remettre le projet et date de la soutenance remportées. Lire ici.
• Soutenances du projet : à lire attentivement.
• Les TPs du 12/12 et 13/12 sont remplacés par les soutenances (12/01/2006).
• L'examen se déroulera le lundi 9 janvier 2006, de 14h00 à 17h00, en Amphi. Documents autorisés.
• Quelques solutions au TD unification.
• État de votre bonus (faisant partie du contrôle continu).
• Les notes du partiel.
• La correction du partiel.
• Le projet.

Références

• Guy Cousineau et Michel Mauny. Approche fonctionnelle de la programmation .
  [B] Collection Informatique. Paris: Ediscience International. xiii, 428 p. (1995). [ISBN 2-84074-114-8; ISSN 0989-392X].
  

• Emmanuel Chailloux, Pascal Manoury and Bruno Pagano. Développement d'applications avec Objective Caml.
• La page web du langage CAML à l'INRIA.
• Michel Mauny. Functional programming using Caml Light.
  

• Glynn Winskel. The formal semantics of programming languages: an introduction.
  [B] MIT Press Series in the Foundations of Computing. London: MIT Press. XI, 361 p. (1993). [ISBN 0-262-23169-7/hbk].
  

Emploi du temps

• 4/10/05 : Caml toplevel, évaluation, définitions, types élémentaires (int, float, bool, string, char), produit cartésiens, espaces de fonctions, fonctions récursives. Notes du cours de/par Solange Coupet, version à imprimer, code utilisé dans le cours.
  Le TD et le TP.

• 10/10/05 : Évaluation par valeur et par nom. Filtrage, polymorphisme, listes. Notes du cours de/par Solange Coupet, version à imprimer, code utilisé dans le cours.
  Le TD et le TP. Correction de l'exercice 3.

• 17/10/05 : Enregistrement. Définition de types. Types récursifs. Sémantique opérationnelle : évaluation dans un environnement. Notes du cours de/par Solange Coupet, version à imprimer. Le code utilisé dans le cours.
  Le TD. Le TP.

• 24/10/05 : Aspects impératifs du langage OCaml. Exceptions. Entrées sorties, fichiers. Références, arrays, enregistrements avec champs modifiables. Séquencement, boucles. Notes du cours de/par Solange Coupet, version à imprimer. Le code utilisé dans le cours.
  La suite : notes (de/par Solange Coupet), version à imprimer, le code.
  Le TD.
  Le module List.

• 31/10/05 : Termes, substitutions, filtrage. Notes du cours de/par Solange Coupet, version à imprimer. Le code utilisé dans le cours.
  Le module Term, des tests, et la documentation.
  Le TD préparation au partiel avec les solutions.
  

• 7/11/05 : Filtrage et Unification. Notes du cours, version à imprimer.
  

• 14/11/05 : Le calcul de la résolution. Démonstration automatique.
  Le TD. Solutions aux exercices 1 et 2.
  

• 21/11/05 : Pas de cours, TD, ni TP ce jours. Le TP du jour 22/11/05 se déroulera régulièrement.
  

• 28/11/05 : Démonstration automatique. Sémantique opérationnelle.
  Notes du cours : introduction, sémantique opérationnelle (version à imprimer). Le TD.

• 5/12/05 : Induction. Notes du cours (version à imprimer).
  Le TD.

• 12/12/05 : Sémantique dénotationnelle. Équivalence entre les sémantiques. Introduction à la théorie des domaines. Notes du cours (version à imprimer).
  Le TD.
  Les TPs du 12/12 et 13/12 sont remplacés par les soutenances (12/01/2006).

Le projet : typage des expressions fonctionnelles

Soutenances du projet : vendredi 20 janvier à 8h30 en salle 110. Date limite pour rendre les projets : dimanche 15 janvier à 20h00.

Modalité de présentation du projet : fichier projet_LDP_vos_logins.tgz, envoyé par émail au résponsables de votre groupe de TP (Paillet ou Santocanale).

Rappelez vous de nous renseigner (par émail) sur la composition de votre groupe (avant le 16 décembre), et de bien signer votre projet.

Outils vus en cours :

• Le module Terme (ici le code).

• Manuel de Camlp4.
• Le ocamlmakefile.

• La compilation : batch et native.
• ocamllex/yacc.

Outils

• Les examens de l'année passée :
  • l'examen de janvier avec son corrigé,
  • l'examen de juin.
• Aides et références pour préparer ce cours et l'examens :
  • Les notes du cours (si vous les avez prises).
  • Partie Caml : les note du cours de Solange Coupet.
  • Partie unification et résolution : à venir.
  • Sémantique des langages de programmation : Winskel, chapitres 2, 3, 4 et 5.

FAQ

• Comment le cours est évalué ?
     NOTE = (3 * max(3*E,(2E+CC)) + PRJ)/4
  où E est le résultat de l'examen final, CC est l'évaluation du contrôle continue, PRJ est l'évaluation du projet informatique.
• Comment utiliser ocaml avec emacs ?
  Pour utiliser le mode tuareg sous emacs, ajouter les linges suivantes à votre .emacs :
  

  ;;tuareg-mode
  (setq auto-mode-alist (cons '("\\.ml\\w?" . tuareg-mode) auto-mode-alist))
  (autoload 'tuareg-mode "tuareg" "Major mode for editing Caml code" t)
  (autoload 'camldebug "camldebug" "Run the Caml debugger" t)

• ... et avec vi(m) ?
  Deux plugin ocaml pour vim : no_1 et no_2. Pour attribuer la touche F4 au parser il suffit d'exécuter :

  nmap -F4- :OCamlSigParseInstruction -RETURN-
  nmap -S-F4- :OCamlSigParseAll -RETURN-

  (merci à Martin Stéphane),

Infos anciennes