Table of Contents

LANGAGES ET TRADUCTEURS – Chapitre 0 Jean-François Monin & Pierre Corbineau, 2023

Présentation

1 Objectifs

  • Qu'est-ce qu'un langage ?
    • Langage Humain : construction culturelle conventionnelle
    • Langage informatique : aussi culturel et conventionnel mais aussi formel/standardisé : ensemble mathématique de suites de caractères admissibles défini par une spécification/norme/description formelle (cf PF)

      En LT on utilisera une représentation arborescente.

  • Comprendre, fabriquer
  • Compilation, traduction, interprétation
  • Analyses lexicales, syntaxiques
  • Sémantique statique (typage…)
  • Sémantique dynamique

Raisonnement : pratique de Rocq

2 Outils

  • Théorie des langages : syntaxe, sémantique
  • Assistant logiciel à la preuve : Rocq Parfait pour définir des langages et raisonner dessus
  • Compilation certifiée : pour apprendre et pour l'industrie

3 Équipe pédagogique

  • Cours/TP : Pierre Corbineau
  • TD/TP : Pierre Corbineau et Martin Bodin

4 Plan général du cours

4.1 Compréhension des outils conceptuels

  • arbres de syntaxe abstraite (AST)
  • récursion structurelle: définir des fonctions récursives
  • raisonnements par récurrence structurelle

4.2 Initiation à Rocq

Rocq est un assistant à la preuve (qui fait autorité dans le monde)

  • on écrit des définitions dans un langage mathématique et fonctionnel proche de OCaml (mais plus complexe)
  • on démontre des théorèmes formules logiques principalement écrites avec l'implication -> et la quantification universelle ∀ preuves assistées par ordinateur
  • Les arbres sont fondamentaux
    • structures de données (listes, AST, …)
    • règles de sémantique
    • démonstration d'un théorème = arbre de preuve
    • langage fonctionnel "Ocaml ++"
    • preuves assistées par ordinateur

4.3 Sémantique formelle de petits langages impératifs

  • sémantique fonctionnelle
  • sémantique opérationnelle à grand pas
  • sémantique opérationnelle à petit pas

4.4 Principes de compilation

  • syntaxe, analyse syntaxique : délégué à PF
  • compilation certifiée

Created: 2025-09-15 lun. 08:01

Validate