LF - Langages formels

2025 - 2026

Planning global

Ressources pédagogiques

CM

• [LF-CM00.pdf] Intro
• [LF-CM01.pdf] Rappels mathématiques
• [LF-CM02.pdf] Alphabets et langages

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), 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

Volume

• CM : 15 heures (10 x 1h30)
• TD : 9 heures (6 x 1h30)
• TP : 6 heures (4 x 1h30)

Horaires

• Tous les enseignements de LC (et LF) 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 6 octobre 2025
  • 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

Evaluation

L’UE est en contrôle continu intégral, avec 3 épreuves :

• Une interrogation d'1h, en séance de TD le lundi matin (date communiquée plus tard)
• Un TP noté de 30 minutes lundi 1er décembre 2025, date à confirmer
• Une interrogation finale d'1h mardi 2 décembre 2025, date à confirmer

Outre ces 3 épreuves, il y aura une épreuve de seconde chance, la date sera précisée ultérieurement. Tout le monde pourra participer à cette épreuve, la note obtenue remplacera la moins bonne des 2 notes d’interrogation obtenues précédement, si elle est supérieure à celle-ci. Le TP noté ne pourra pas être remplacé par l’E2C.

Règles concernant les absences aux contrôles :

• Zéro à l’épreuve en cas d’absence, qu’elle soit justifiée ou non,
• En cas d’absence justifiée ou non à une épreuve, la note de l’E2C remplacera cette absence,
• En cas d’absences justifiées à deux épreuves ou plus, nous pourrons proposer des épreuves de substitutions, au cas par cas.