Langages et Traducteurs (LT INFO4)
∼∼∼
Consignes pour installer l'environnement de travail
Consignes générales pour les travaux à rendre sur chamilo
Remarque pratique : les fichiers .org sont plus agréables à lire avec emacs (couleurs, navigation, etc.)
∼∼∼
1 Cours
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.
#+BEGIN_2BREMOVED
TODO Correction - Problèmes
- DONE this index.html generated from .org ;
- DONE add annotation "Made with Org-mode" ;
- TODO add +AUTHOR TAG
- TODO coq -> rocq in text and source file name coq*.v -> rocq*.v ;
- DONE in index.org files ".html" are now "link" ;
- DONE clean files enumerations ;
- DONE add ornement paragraph divider ∼∼∼ ;
- DONE add emphasis and =monospace= some part ;
- DONE remove the validator link which is no more valid!
- DONE ??? QUESTION Should we keep the index in all html generated from .org ??? -> NO
- DONE ??? QUESTION standardization of the AUTHOR tag (Jean-François Monin AND Pierre Corbineau ???
- TODO PBR URL ds chap_04_adp : http://www-verimag.imag.fr/~monin/EnseignementPublic/PEIP/Raisonnement_Structure/
- TODO PBR ref biblio ds chap_06_While : ref [Nielson&Nielson] ???
- TODO FILE NOT FOUND file:cours07_inversion.v ds chap_07_inversion
- TODO chap_06 section 3 VIDE : "3 Propriétés issues de la SN"
#+END_2BEREMOVED
∼∼∼
Made with Org-mode