Curriculum LDD Informatique-Mathématiques
Cours : Programmation -- concepts et fondements (S1)
Objectifs : Ce cours est d'abord une introduction aux différents paradigmes des langages de programmation, des constructions typiques de ces langages et de ce qui fait que certains sont dits impératifs et d'autres fonctionnels par exemple. Il y sera question de portée (lexicale, opposée à la liaison dynamique), de passage de paramètres, de constructions de types de données, de compilation et de représentation en mémoire des objets. La définition formelle des langages de programmation (lexique, syntaxe et sémantique) sera abordée en utilisant les notions d'expressions régulière, de grammaire non-contextuelles et de traduction et interprétation orientées par la syntaxe. Ces notions seront mises dans le contexte d'un interpréteur ou d'une chaine de compilation. La question de savoir ce qu'un programme fait mènera à la notion de sémantique, opérationnelle ou dénotationnelle. On évoquera comment ces sémantiques justifient la correction de logiques comme la logique de Hoare. La notion de systèmes de types sera étudiée, et notamment le fait qu'un programme bien typé offre des garanties d'absence d'erreurs à l'exécution.
Plan détaillé :
- Paradigme de langages de programmation: impératif, fonctionnel, orienté-objet, logique, concurrent avec des exemples en C, C++, Java, OCaml, Prolog et Python.
- Définition des langages de programmation: expressions régulières étendues (lexique), grammaires non-contextuelles (syntaxe), arbre de syntaxe abstraite et traduction dirigée par la syntaxe. Chaîne de compilation.
- Coeur impératif: contrôle structuré et non-structuré, graphe de flot de contrôle, expressivité (théorème Peterson, Kasami et Tokura); variables et expressions, portée et ordre d'évaluation; types de données et gestion de la mémoire; polymorphisme; fonctions et procédures, passage de paramètres, élimination de la récursivité terminale, représentation en machine.
- Programmation à grande échelle: classes et modules en C++ et OCaml.
- Programmation fonctionnelle: types algébriques, polymorphisme, inférence de types, filtrage des valeurs, effets impératifs, (de-)curryfication; en OCaml et Lisp.
- Programmation logique: calcul de prédicats, recherche de preuve, unification et substitution, coupures en Prolog.
- Programmation concurrente: fil d'exécution et processus, synchronisation par messages, mémoire partagée et signaux.
- Sémantique opérationnelle.
- Sémantique dénotationnelle, correction, adéquation, d'abord pour un langage impératif simple, ensemble pour un langage fonctionnel simple d'ordre supérieur;
- Logiques sur les programmes: logique de Hoare, plus faibles préconditions de Dijkstra, continuations.
- Systèmes de typage, inférence de types simples, unification, typage en ML, et garanties d'absences d'erreurs à l'exécution.
Références :
- Ravi Sethi. Programming Languages : Concepts and Constructs. 2eéd. Addison-Wesley, 1996. isbn : 978-0321210746
- Brian Kernighan et Dennis Ritchie. The C programming language. PrenticeHall, 1988. isbn : 978-0-13-110362-7
- Glynn Winskel. The formal semantics of programming languages - an introduction. Foundation of computing series. MIT Press, 1993. isbn : 978-0-262-23169-5
- Notes de cours seconde partie, lien "Programming and Semantics".