LifLF - Langages formels
ANNEE 2023 - 2024
Planning global
Progression et ressources pédagogiques
| 1 | lundi 04/09/23 | 9h45-11h15 | CM0 | Introduction | [slides] |
| CM1 | Rappels maths | [slides] | |||
| mardi 05/09/23 | 14h-15h30 | CM2 | [[Alphabets et langages | [slides] | |
| 2 | lundi 11/09/23 | 9h45-11h15 | TD1 | Ensembles et relations | [sujet] |
| mardi 12/09/23 | 14h-15h30 | CM3 | Grammaires | [slides] | |
| 3 | lundi 18/09/23 | 9h45-11h15 | TD2 | Alphabets, langages, représentation finie | [sujet] |
| mardi 19/09/23 | 14h-15h30 | CM4 | Automates à états finis | [slides] | |
| 4 | lundi 25/09/23 | 9h45-11h15 ou 11h30-13h | TP1 | Prog. fonctionnelle en Coq / Gallina | [sujet] [tp1.v] [tp1_cor.v] |
| mardi 26/09/23 | 14h-15h30 | CM5 | Déterminisation | [slides] | |
| 5 | lundi 02/10/23 | 8h-9h30 | TD3 | Automates à états finis - déterminisation | [sujet] |
| mardi 03/10/23 | 14h-15h30 | CM6 | Caractérisation | [slides] | |
| 6 | lundi 09/10/23 | 9h45-11h15 ou 11h30-13h | TP2 | Automates en Coq (part. 1) | [sujet] [tp2.v] [tp2_cor.v] |
| mardi 10/10/23 | 14h-15h30 | CM7 | Minimisation des états | [slides] | |
| 7 | lundi 16/10/23 | 8h-9h30 | TD4 | Caractérisation - automate standard | [sujet] |
| mardi 17/10/23 | 14h-15h30 | CM8 | Langages rationnels - rationalité | [slides] | |
| 8 | lundi 23/10/23 | 9h45-11h15 ou 11h30-13h | TP3 | Automates en Coq (part. 2) | [sujet] [tp3.v] [tp3_cor.v] |
| mardi 24/10/23 | 14h-15h30 | CM9 | Automates à pile - algébricité | [slides] | |
| Vacances universitaires | |||||
| 9 | lundi 06/11/23 | 8h-9h30 | TD5 | Lemme d’Arden - rationalité | [sujet] |
| mardi 07/11/23 | 14h-15h30 | CMA | Analyse ascendante | [slides] | |
| 10 | lundi 13/11/23 | 9h45-11h15 | TD6 | Grammaires - analyse ascendante | [sujet] |
| 11 | lundi 20/11/23 | 9h45-11h15 ou 11h30-13h | TP4 | Grammaires et automates en Coq | [sujet] [tp4.v] [tp4_cor.v] |
| 12 | lundi 27/11/23 | (pas d’enseignements de langages) | |||
| 13 | lundi 04/12/23 | 8h-13h | TPN | TP noté | |
| mardi 05/12/23 | 14h-15h30 | ECA | Epreuve commune anonyme |
Instructions pour les TP
-
On utilise Coq depuis une IDE (CoqIDE, VSCode, EMACS …).
-
Lancez votre IDE :
- CoqIDE, disponible sur les machines des salles de TP du campus (Linux uniquement)
- VSCode, disponible sur les machines des salles de TP du campus, nécessite d’installer l’extension VsCoq avec la version 0.3.9
- EMACS avec Proof General …
-
Téléchargez le fichier .v (lien ci-dessus dans la progression), ouvrez-le dans votre IDE, lisez le sujet et complétez le fichier.v dans votre IDE.
Alternative à une IDE : JsCoq ; Collez le sujet du TP dans le cadre de gauche
Pour voir correctement le sujet dans votre navigateur, configurez l’encodage par défaut de votre navigateur en Unicode (UTF-8)
Pour travailler sur votre machine personnelle
Pour installer CoqIDE sur votre machine
Les installeurs de CoqIDE incluent Coq.
-
MacOS :
- Installeur binaire sur https://github.com/coq/platform/releases/latest (inclut CoqIDE)
- Avec Homebrew :
brew install coqide
-
Windows : plusieurs manières d’installer CoqIDE, cf. Installer Coq sous Windows :
- Installeur binaire sur https://github.com/coq/platform/releases/latest (inclut CoqIDE)
- Installer Linux dans une VM ou dans WSL puis suivre les instructions pour Linux
-
Linux : cf. Installer Coq sous Linux (de préférence avec opam)
Pour utiliser Coq avec VSCode
- Installez Coq (cf. ci-dessus)
- Installez l’extension VsCoq dans VSCode, précisez version 0.3.9.
Organisation
Responsables
- LifLF - Théorie des langages formels : Sylvain Brandel
- LifLC - Logique classique : Xavier Urbain, page pédagogique de logique classique
Volume
- CM : 15 heures (10 x 1h30)
- TD : 9 heures (6 x 1h30)
- TP : 6 heures (4 x 1h30)
Horaires
- Tous les enseignements de LifLF (et LifLC) ont lieu dans la séquence 1 (lundi matin et mardi après-midi)
- Globalement, les CM ont lieu le mardi après-midi de 14h à 15h30, les TD / TP le lundi matin de 8h à 9h30 et de 9h45 à 11h15 ou de 11h30 à 13h ; chaque créneau de 8h à 9h30 et de 9h45 à 11h15 ou de 11h3à à 13h est occupé soit par un TD / TP de théorie des langages, soit par un TD / TP de logique classique
- À partir du 25 septembre 2023
- TD de LC ou de LF de 8h à 9h30
- TP de LC ou de LF de 9h45 à 11h15 ou de 11h30 à 13h
- Fiez-vous à votre emploi du temps sur ADE
Intervenants
- Sylvain Brandel (CM, TD et TP groupe A)
- Emmanuel Coquery (TD et TP groupe B)
- Fabien De Marchi (TD et TP groupe C)
- Xavier Urbain (TD et TP groupe D)
- Mohand-Said Hacid (TD groupe E)
- Romuald Thion (TP groupe E
Evaluation
- Contrôle continu intégral :
- TP noté lundi 4 décembre 2023 8h ou 9h45
- ECA mardi 5 décembre 2023 14h
- Interros en début de TD, peut-être un autre TP noté …
- Rattrapage en juin 2024
- Règles d’absences aux contrôles de TD :
- Zéro en cas d’absence à un contrôle de TD, justifiée ou non, quelle qu’en soit la raison
- Pas de rattrapage des contrôles en cas d’absence (légère tolérence au retard)
- La moyenne des n contrôles sera calculée à partir des (n-1) meilleures notes
- Le jury d’UE discutera des cas particuliers (absence longue durée, absences répétées …)