Enseignement

 

Specifying and Prototyping using Higher Order Logics at ESSLLI

I'm a lecturer at the ESSLLI 2012 summer school. See the dedicated webpage of the course.

Advanced Models for Programming à ITU Copenhagen

In 2012, I'm a co-lecturer (15%) for this intensive master course (15 ECTS) at the IT University of Copenhagen. I've been teaching type systems, and more particularly type inference, various OO styles, Featherweight Java, subtyping, and applications to XML programming. In addition, I'll be supervising projects at the end of the semester.

Compilation à Paris-Sud

Pour le premier semestre 2011/2012, j'ai pris en charge 25h de TD pour le cours de compilation du M1 pro Informatique. Toutes les informations sont sur la page du cours.

Mathématiques pour l'Informatique à Paris-Sud

Pour le second semestre 2010/2011, j'ai pris en charge 20h de TP Coq pour ce cours de L2. Toutes les informations sont sur la page du cours.

 

Monitorat à l'École Polytechnique

Dans le cadre de mon monitorat à l'École Polytechnique, j'ai encadré les travaux pratiques des cours suivants:

 

TP OCaml en MPSI

Second semestre 2005/2006, lycée Janson de Sailly.

N'hésitez pas à m'envoyer vos questions, remarques, souhaits. Je réponds à mes mails.

  1. Premiers pas

    Comprendre les types; curryfication; trouver un habitant d'un type; types variants; la représentation binaire des entiers strictement positifs, traductions et addition; le triangle de Pascal. Télécharger: Postscript | PDF | TeX.

  2. Arbres dictionnaires

    Listes associatives triées; arbres comme dictionnaires; préfixes univoques minimaux. Télécharger: Postscript | PDF | TeX | Corrigé Caml.

  3. Programmation dynamique

    Introduction à la programmation dynamique et application à la recherche de la plus longue sous-liste commune. Télécharger: Postscript | PDF | Corrigé.

  4. Problème des Reines

    Utilisation des fonctions standard du module List; compréhension de code impératif; problème des reines. Télécharger l'énoncé et le corrigé mis à jour: Postscript | PDF | TeX | Corrigé.

  5. Labyrinthes

    Génération aléatoire de labyrinthes connexes minimaux, recherche du plus court chemin. L'énoncé a été revu, de nouvelles instructions se trouvent dans le code source à télécharger. Télécharger l'énoncé: Postscript | PDF | TeX; le code des définitions et du module graphique: ML; le corrigé: corrigé.

  6. Sudoku

    Résolution "déductive" du jeu de Sudoku. Télécharger l'énoncé: Postscript | PDF | TeX; le code des définitions: ML; le corrigé: ML.

  7. TP "libre-service"

    Je réponds aux questions. On peut finir d'anciens TPs, ou travailler sur le sujet (a priori rassurant) de l'X2002.

Pour la suite...

Si vous cherchez à travailler la prog de votre côté, il y a pas mal de choses à faire. Vous pouvez finir les TPs. Les sujets de l'X (disponibles en ligne) contiennent beaucoup de questions de programmation, de difficulté progressive. Par contre, les correcteurs sont exigeants sur la rédaction des réponses. Entrainez-vous à écrire des algorithmes simples et clairs (refaire les bases encore et encore ne serait pas inutile pour la plupart) et à les prouver. Les preuves d'algorithmes simples sont souvent simples, mais il faut bien les formuler.

Si vous en avez marre de prouver des algorithmes, vous pouvez jeter un oeil à un bouquin de théorie des graphes, c'est un très bon exercice de rédaction de preuve formelle de résultats intuitifs. Autres pistes d'exercices de prog, ou même de TIPE:

Pas de lien sur tous ces sujets, mais vous devriez pouvoir vous renseigner un minimum sur Internet pour la plupart. A la demande, je peux approfondir un point.