~~NOTOC~~

====== Sémantique des langages de programmation ======

===== Description =====

Quel est le comportement de ce fragment de code informatique ? Puis-je toujours le remplacer
par tel autre sans changer le sens du programme complet ? Comment m’assurer systématiquement de l’ab-
sence de certaines classes d’erreurs à l’exécution ? Ces questions sont essentielles à la pratique quotidienne
de la programmation comme à la conception d’outils manipulant du logiciel (compilateurs, analyseurs
statiques, éditeurs de code intelligents, etc.). Y répondre précisément exige le développement d’une théorie
mathématique du sens des programmes. Ce module offre les bases de cette théorie, la sémantique des
langages de programmation.

===== Syllabus =====

==== Sujets centraux ====

  * Syntaxe abstraite, liaison et α-conversion, substitution.
  * Réécriture et évaluation.
  * Sémantique dénotationnelle.
  * Relations logiques.
  * Équivalence de programmes.
  * Langages objets : système T, PCF.
==== Sujets potentiellement traités ====

  * Autre langages objets : λ-calcul pur, λ-calcul effectif, système F.
  * Stratégies d’évaluation : appel par nom, par valeur, par pousse-valeur.
  * Effets calculatoires : affichage, état global, erreurs.
  * Théorie de la réécriture pour le λ-calcul pur
===== Pré-requis =====

  * [[..:..:..:licence:2024-2025:ue:l3:md5|Mathématiques discrètes]] de la licence.
    * Définitions et raisonnement par induction.
    * Manipulations élémentaires sur les ensembles.
    * Relations d'ordre.