Objectifs détaillés

Pré-requis

Ce chapitre vise à introduire des notions mathématiques nécessaires pour pouvoir assimiler les notions principales traitées par le module. Ainsi, à la fin de ce chapitre :

• L'étudiant a fait un rappel sur les différentes notions liées aux langages de programmation et aux paradigmes de programmation.
  
• L'étudiant est capable de lire la définition d'un système formel.
• L'étudiant est capable d'écrire des preuves dans un système formel donné.
• L'étudiant a fait une étude sur la théorie du point fixe.

Lambda-Calcul et Lambda-Calcul typé

A la fin de ce chapitre, l'étudiant va être en mesure de :

• Définir, présenter et expliquer le lambda-calcul
• Evaluer des expressions en Lambda-Calcul (notamment la béta-réduction).
• Illustrer la notion de calculabilité en Lambda-Calcul.
• Ecrire des programmes en Lambda-Calcul.
  

Logique classique et Intuitionniste

A la fin de ce chapitre, l'étudiant sera capable de :

• Présenter la logique intuitionniste.
• Distinguer et comparer entre la logique classique et la logique intuitionniste.
• Ecrire des preuves dans la logique intuitionniste.

Sémantique formelle

L'objectif de ce chapitre est de présenter les notions théoriques liées à la sémantique formelle des langages de programmation. Ainsi, à la fin de ce chapitre, l'étudiant va être capable de :

• Définir la notion de la Sémantique Formelle.
• Expliquer les objectifs et l'apport de la Sémantique Formelle.
  
• Citer, détailler et illustrer les différents types de sémantiques formelles

Expression formelle de sémantiques

Ce chapitre couvre la partie pratique des notions théoriques présentées dans le chapitre précédent. A la fin de ce chapitre, l'étudiant va être capable de :

• Lire la spécification formelle d'un langage de programmation.
• Ecrire des preuves de programmes en utilisant la sémantique formelle.
• Adapter et modifier une spécification pour changer les caractéristiques d'un langage de programmation.
• Ecrire des preuves dans un environnement de preuves comme Coq.