Pierre Letouzey

MV6 : Machines Virtuelles (Licence 3)

Support de cours et de TP:

• Cours1 : pdf ps
• Cours2 : pdf ps
• Cours3 : pdf ps
• Cours4 : pdf ps
• Cours5 : pdf ps
• Les 5 cours regroupés en un document imprimable : pdf ps
• TD1-3: réalisation d'une machine virtuelle pour UMIX (concours ICFP2006).
  • Les fichiers supports pour ce TP.
  • Pour en savoir plus, le site web du concours de programmation ICFP2006.
• TD4: manipulation de bytecode caml. Sujet: pdf ou ps.
• TD5: bytecode Caml, suite (extrait de l'examen 2007). Sujet: pdf ou ps.
• TD6: manipulation de bytecode java. Sujet: pdf ou ps.
• Annales: le sujet de juin 2007 en pdf ou ps.

Références:

• Une description des instructions du bytecode Caml par X. Clerc
• La spécification de la JVM. Une liste condensée et imprimable des instructions de la JVM.

Pour vous aider à étudier le bytecode Caml, les outils suivants sont à votre disposition sur lucien:

• Pour demander à caml comment il compile une phrase donnée en bytecode, lancer ocaml -dinstr puis entrer votre phrase.
• Pour voir l'évolution de la pile et de pc au cours de l'execution d'un morceau de bytecode, mettre ce bytecode dans un fichier test et lancer interp_byte test. Le bytecode doit utiliser la même syntaxe que celle affichée par ocaml -dinstr, et provenir d'une phrase autonome, contenant uniquement des instructions vu en cours. En particulier, pas d'accès à des variables ou fonctions globales...
• Il est possible de créer un véritable fichier test.cmo à partir d'un fichier test contenant du bytecode au format texte tel que produit par ocaml -dinstr. Pour cela, lancer byte2cmo test. Cela produit un fichier (toujours) nommé test.cmo. On peut ensuite exécuter ce test.cmo avec la commande runcmo test.cmo (qui n'est autre qu'un appel déguisé à ocaml). En partant d'une phrase autonome Caml ... on ne voit alors rien, car il n'y a aucun affichage. Heureusement, ce byte2cmo accepte lui de traiter au moins les accès globaux aux fonctions de Pervasives, telles que print_int. Si la fonction qui vous intéresse produit un entier, vous pouvez par exemple placer le code que voici devant le votre, ce qui déclenchera un affichage de l'entier.
• Enfin, à partir d'un fichier test.cmo il est possible d'afficher le bytecode contenu dedans avec la commande cmo2byte test.cmo

Enfin, pour les curieux et les aventureux, voici les sources de mon interp_byte : ma_cvm.tgz. Sur un système digne de ce nom, il n'y a normalement qu'à désarchiver, aller dans le sous-répertoire, taper make, puis renommer le binaire main en interp_byte.

Compilation (Master 1)

See the main web site of this course.

Preuves Assistées par Ordinateur (Master 1)

Notes de cours (préparées par Alexandre Miquel)

• Le document principal
• Le système T de Gödel
• La théorie des types simples de Church
• Un petit guide de survie pour Coq

Quelques autres polycopiés concernant le lambda-calcul:

• Par Délia Kesner
• Par Jean-Jacques Lévy
• Par Emmanuel Chailloux
• Par Gilles Dowek

Sujets des TD/TP:

• TD1 (déduction naturelle): pdf
• TD2 (arithmétique de Peano): pdf
• TD3 (premiers pas en Coq): pdf
• TD4 (maths élémentaires en Coq): pdf
• TD5 (entiers naturels en Coq): pdf
• TD6 (théories et modèles): pdf
• TD7 (listes en Coq): pdf
• TD8 (prédicats inductifs): pdf
• TD9 (enigme de MU): pdf
• TD10 (système T et théorie des types simples): pdf

Annales:

• Sujet de 2005
• Sujet de 2006

Projet: le sujet en pdf, le fichier fourni MoreString.v et le fichier fourni à compléter LZW_skel.v

Preuves de Programmes (Master 2 LC)

Fichiers montrés en cours

• cours1_contretest.ml
• cours2_programmation_coq.v
• cours3_types_inductifs.v
• cours4_predicats_inductifs.v

Sujets des TP:

• TP1 (premiers pas en Coq): pdf
• TP2 (entiers naturels en Coq): pdf
• TP3 (définitions inductives en Coq): pdf
• TP4 (arbres binaires de recherche): pdf
• TP5 (fonctions partielles en Coq): pdf
• TP6 (logique de Hoare): pdf
• TP7 (logique de Hoare, suite): pdf

Projet: enoncé

Anciens cours

Me contacter.