Sémantique des langages de programmation
Cours : Daniel Hirschkoff (Daniel.Hirschkoff)
TP : Stephane Leroux (Stephane.Leroux)
Cours de base (30 h de cours, 30h de TD)
Présentation
Ce cours a pour but d'introduire les techniques classiques de
modélisation sémantique des langages de programmation, en liaison avec
les autres cours, notamment ceux de Programmation et de Compilation.
Ce faisant, il s'agit également d'introduire les modèles sémantiques
du calcul séquentiel et parallèle que sont le λ-calcul et des
algèbres de processus telles CCS et le π-calcul.
Ce cours nécessite une connaissance basique du λ-calcul et des
notions de logique; il s'adresse à toute personne curieuse de
comprendre la structure des langages de programmation et les
bases conceptuelles de la programmation et d'abstraire certains
concepts appréhendés jusque-là essentiellement de leur point de vue
pragmatique.
Plan indicatif
L'objet de la sémantique est fondamentalement d'associer du sens
à des composants d'un langage. Pour nous ce seront les
différents éléments d'un programme. Le sens est un objet
mathématique à définir, sur lequel on peut faire des manipulations
formelles et des preuves.
Ce cours s'intéressera en premier lieu aux langages séquentiels. Nous
présenterons les différentes manières de définir la sémantique d'un
programme que sont:
-
La sémantique opérationnelle
- on associe à un programme la
suite des états d'une machine (abstraite) qui l'exécute.
- La sémantique dénotationnelle:
- on associe à un programme la
fonction mathématique qu'il calcule.
- La sémantique axiomatique:
- on associe à un programme
l'ensemble des assertions logiques reliant ses sorties et ses
entrées.
Ces approches seront développées sur un petit langage impératif, et,
pour certaines d'entre elles, étudiées de manière plus approfondie sur
le λ-calcul.
Dans une seconde partie du cours (de taille moindre), nous montrerons
comment les approches développées pour le calcul séquentiel se
conçoivent dans un contexte parallèle. Nous introduirons notamment le
Calculus of Communicating Systems et le π-calcul, et nous
présenterons les notion d'équivalence comportementale et de
bisimulation.
Bibliographie
- G. Winskel, The formal semantics of programming languages: an
introduction. MIT Press, 1993.
- J. Reynolds, Theories of Programming Languages, Cambridge
University Press.
- J.-Y. Girard, Y. Lafont and P. Taylor, Proofs and Types,
Cambridge Tracts in Theoretical Computer Science.
- Robin Milner. Communication and Concurrency, Prentice Hall.
- Robin Milner. Communicating and Mobile Systems: the pi-Calculus,
Cambridge University Press, May 1999.
- Roberto Amadio and Pierre-Louis Curien. Domains and
Lambda-Calculi, Cambridge Tracts in Theoretical Computer Science,
n° 46, Cambridge University Press, 1998.
- B.A. Davey and H.A. Priestley. Introduction to Lattices and Order.
Cambridge Math. Textbooks, 1990.
- C. Livercy. Théorie des Programmes (schémas, preuves,
sémantique). Dunod, 1978.
http://www.ens-lyon.fr/ plescann/Livercy