Cette UE a pour objectif l'étude des théories des types qui fondent les langages de spécification formelle et les méthodes de preuve de correction du logiciel. Une place importante est réservée à l'étude des propriétés logiques et mathématiques de ces théories. La manipulation de différents systèmes d'aide à la preuve permet de comprendre leur mise en oeuvre. Enfin, leur utilisation dans les outils de compilation ou d'édition de liens sont aussi présentées.
