Etude des systèmes de types ensemblistes

Etude des systèmes de types ensemblistes. Écrire des programmes corrects et prouver leur exactitude est une tâche pleine de défis. Pour appréhender ce problème, les langages de programmation modernes sont équipés d’un système de typage. Les types sont des constructions syntaxiques semblables à des formules logiques qui permettent aux machines de vérifier automatiquement si les programmes respectent les types et ne produisent pas une certaine classe d’erreurs à l’exécution. Ici, les types sont étudiés en les interprétant comme des ensembles de valeurs d’un langage de programmation.