• Principes de base des langages de programmation
  
  
• Initiation à la vérification
  
  
• Programmer + un peu de théorie

• cours: JJL, INRIA - Rocquencourt
• TD:

  	Fabrice le Fessant, AMX, INRIA; Compaq SRC
  	Alan Schmitt, AMX, INRIA

• langages impératifs = sémantique opérationnelle (mémoire)
• langages fonctionnels = l-calcul
• langages objets = calcul Abadi/Cardelli
• programmation logique = logique du premier ordre
• concurrence = mémoire partagée + CCS/p-calcul
• distribution ou mobilité = ??
  
• méthodes des assertions = logique de Hoare

• modèles
• types
• interprétation
• compilation (® majeure M2)
• analyse statique
• démonstration mécanique / automatique

• langages spécifiques ® Airbus + réseaux actifs
• types ® allocation mémoire automatique
• analyse statique ® logiciel de bord Ariane 5 + an 2000
• vérification mécanique ® lignes 14 + A de la Ratp

• langages fonctionnels
• types
• modèles de la mémoire
• allocation mémoire
• programmation logique
• assertions logiques

• Réducteur/Interpréteur de PCF
• Vérificateur/Synthétiseur de types
• Mini-ML avec références et objets

• Programming Languages, Concepts and Constructs, Ravi Sethi, 2nd edition, 1997. http://cm.bell-labs.com/who/ravi/teddy/
  
  
• Theories of Programming Languages, J. Reynolds, Cambridge University Press, 1998. http://www.cs.cmu.edu/afs/cs.cmu.edu/user/jcr/www/
  
  
• Type Systems for Programming Languages, Benjamin C. Pierce, Cours University of Pennsylvania, 2000. http://www.cis.upenn.edu/~bcpierce/
  
  
• Programming Languages: Theory and Practice, Robert Harper, Cours Carnegie Mellon University, Printemps 2000. http://www.cs.cmu.edu/~rwh/
  
  
• Notes du cours de DEA ``Typage et programmation'', Xavier Leroy, Cours de DEA, Décembre 1999, http://pauillac.inria.fr/~xleroy/dea

This document was translated from L^AT_EX by H^EV^EA.