Ci-dessous, les différences entre deux révisions de la page.
| Les deux révisions précédentesRévision précédente | |||
| formations:masters:ue:m1:sem8 [2025/01/29 10:44] – ↷ Liens modifiés en raison d'un déplacement. admin | formations:masters:ue:m1:sem8 [2025/01/29 10:46] (Version actuelle) – ↷ Liens modifiés en raison d'un déplacement. admin | ||
|---|---|---|---|
| Ligne 1: | Ligne 1: | ||
| + | ~~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, | ||
| + | statiques, éditeurs de code intelligents, | ||
| + | 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, | ||
| + | * 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 ===== | ||
| + | |||
| + | * [[..: | ||
| + | * Définitions et raisonnement par induction. | ||
| + | * Manipulations élémentaires sur les ensembles. | ||
| + | * Relations d' | ||