Résumé
Qu'il soit vérifié dynamiquement (pendant l'exécution) ou statiquement (par analyse préalable), le typage est un aspect essentiel des langages de programmation de haut niveau. Dans ce cours, nous étudierons les contributions du typage à la sécurité des logiciels, des garanties de base (sûreté des valeurs et de la mémoire) indispensables pour l'isolation logicielle à des garanties plus fines s'appuyant sur l'abstraction de types. Nous parlerons aussi des types pour la gestion des ressources (types d'unicité, types linéaires, possession et emprunts) et de leurs utilisations possibles pour la sécurité.
