INFO3210 : Projet fonctionnel

Ce cours est avant tout un cours projet, durant lequel on développe un interprète pour un langage fonctionnel relativement riche. C'est l'occasion de découvrir par la pratique un certain nombre de notion entrant en jeu dans le contexte de la compilation. Pour les binômes les plus avancés, l'implémentation d'un petit assistant de preuves est également prévue.
Un tiers environ du cours est consacré à une partie théorique, qui se focalise sur le lambda-calcul typé, ses liens avec les langages de programmation (systèmes de types avancés, garanties offertes par le typage) et avec la logique (théorie de la démonstration, idées sous-tendant la définition d'assistants de preuve).