Systèmes de Types et Programmation

Programmer, c'est transcrire un problème algorithmique dans un langage particulier. Cette opération n'est pas univoque (plusieurs façons de faire) et potentiellement hasardeuse (plusieurs façons de se tromper). De quels outils un programmeur dispose t'il pour l'assister dans cette transcription ? Quelles formes de vérification automatique existent qui permettent de certifier des propriétés d'un programme ?
L'un des outils les plus généralisés et directement applicables utilisés par les programmeurs pour vérifier leur code, ce sont les systèmes de types. Ce cours va s'intéresser à :

définir et comprendre ce qu'est un système de type,
comprendre les algorithmes permettant de vérifier la correction des types,
étudier les formes classiques de polymorphisme, des manières de manipuler des types distincts de façon uniforme,
examiner des formes plus avancées de vérification, allant jusqu'aux preuves de programmes.

Ce cours examine les langages de programmation de manière transverse, et prend des exemples variés dans des langages tels qu'Haskell, OCaml, et Scala (entre autres) en plus des classiques que sont le C, C++ et Java. Il aborde le problème d'un point de vue formel, en se ramenant systématiquement au modèle fondamental du lambda-calcul simplement typé. L'idée essentielle reliant ces concepts est leur caractère applicable, permettant de programmer et de certifier, sans avoir à écrire directement des preuves.

Connaissance des langages de programmation C, C++, Java, Scheme.

Aborder les problématiques de typage, de polymorphisme et de preuve de programme.