Types d'affinage : Pratique et sonorité

Cette séance de cours explore la praticabilité et la solidité des types de raffinement, qui améliorent les types de langage de programmation avec des prédicats logiques pour des spécifications plus expressives. L'instructeur présente les types de raffinement de Liquid Haskell, en discutant de leur praticabilité, de leur généralité, de leur expressivité et de leur solidité. La séance de cours porte sur des sujets tels que l'indexation sûre, la vérification des propriétés de la lumière et la vérification de spécifications plus profondes comme la préservation du type. De plus, la séance de cours se penche sur la vérification de la lumière et des propriétés profondes à l'aide de Liquid Haskell, soulignant les défis et les avantages de l'utilisation des types de raffinement dans la vérification du programme.