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.

• 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.

• 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

• Mathématiques discrètes de la licence.
  • Définitions et raisonnement par induction.
  • Manipulations élémentaires sur les ensembles.
  • Relations d'ordre.