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. Le cours a étudié 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 d’intégrité plus fines s’appuyant sur l’abstraction de types et sur le typage statique des ressources et de leur possession (ownership et borrowing, comme dans le langage Rust). Nous avons ensuite montré comment appliquer le typage statique à du code mobile, par vérification de code intermédiaire (comme le bytecode JVM du langage Java) ou de code machine, allant jusqu’à la notion très générale de code auto-certifiant (proof-carrying code).
