Objectifs de l’enseignement

Ce cours permet d'acquérir une bonne connaissance des significations pouvant être attribuées aux constructions syntaxiques de programmes, des méthodes de raisonnement et de validation des programmes. Il forme à la conception et au développement raisonné d'applications et facilite la compréhension des choix et modes de fonctionnement des outils et ateliers de développement.

Contenu de la matière

• Théorie du Lambda Calcul
• Théorie des Combinateurs
• Théorie des types
• Exemples de types : Le langage Caml
• Théorème de Curry-Howard
• De Caml vers Ocaml
• Preuves de propriétés avec Coq
• Les systèmes de certification : FocaL, B, ..