Langages et Traducteurs (LT INFO4)
∼∼∼
Consignes pour installer l'environnement de travail
Consignes générales pour les travaux à rendre sur Moodle Grenoble INP
Remarque pratique : les fichiers .org sont plus agréables à lire avec emacs (couleurs, navigation, etc.)
∼∼∼
1. Cours
1.1. Planning général, fichier .org
1.2. Supports de cours textuels
- Chapitre 0 présentation, fichier .org ;
- Chapitre 1 fonctions, fichier .org ;
- Chapitre 2 arbres, fichier .org
- Chapitre 3 égalités, fichier .org ;
- Chapitre 4 arbres de preuve, fichier .org ;
- Chapitre 5 relations inductives, fichier .org ;
- Chapitre 6 langage While, fichier .org ;
- Chapitre 7 égalités super-contagieuses, inversions, fichier .org ;
- Chapitre 8 sémantique opérationnelle structurelle de While, fichier .org.
1.3. Supports de cours en Rocq
- B A BA, fichier rocq ;
- B A BA en mode interactif, fichier rocq ;
- B A BA avec fonction "ouf", fichier rocq ;
- Récurrence sur propriété quantifiée (
éventuellement partagé avec PF), fichier rocq; - Égalité booléenne sur nat, fichier rocq ;
- Sémantique naturelle du langage While : définition, fichier rocq ;
- Polymorphisme, arguments implicites, fichier rocq ;
- Sémantique naturelle du langage While : propriétés (début), fichier rocq ;
- Égalités super-contagieuses, inversions, fichier rocq ;
- SOS du langange While, fichier rocq.
∼∼∼
2. TD
Consignes générales pour les travaux à rendre sur chamilo
- TD 01 - Grammaires d'expressions, (
répondre dans lefichier .org,aide :TD 01 dessin) ; - Énoncé TD 02 : fichier rocq
à rendre en devoir à la maison; - Énoncé TD 03 : fichier rocq
à rendre en devoir à la maison;
(Attention: il y a desquestions facultativesà différents endroits, elles ne sont pas regroupées à la fin,
NE PASles traiter avant que le reste ait été fait, laissez les "Admitted" puis revenez-y dans un second temps en fonction de votre temps disponible) ; - Énoncé TD 04 : fichier rocq
à rendre en devoir à la maison; - Énoncé TD 05 partie 1 (relations inductives) : fichier rocq
à regarder pour le TD5; - Énoncé TD 05 partie 2 (sémantique de While) : fichier rocq
à rendre en devoir à la maison; - Énoncé TD 06+ (sémantique naturelle) : fichier rocq.
à rendre en devoir à la maison en plusieurs étapes; - Énoncé TD 07 (sémantique opérationnelel structurelle) : fichier rocq (
avec notamment le matériel à réutiliser dans le projet final) ; - Énoncé TD 08 (compilation certifiée) : fichier rocq (
Compiler préalablement les définitions préliminaires: fichier rocq).
∼∼∼
3. Projet
Partagé avec Programmation Fonctionnelle. Aller ici.