Séance de cours

Programmation Fonctionnelle Vérifiée : Nicolas Voirol défense de thèse de doctorat publique

Description

Cette séance de cours couvre le concept de programmation fonctionnelle vérifiée, soulignant l'importance de la vérification formelle dans le développement de logiciels pour prévenir les bogues catastrophiques. Il explore les défis de la vérification des programmes, les avantages de la programmation fonctionnelle et l'utilisation des résolveurs SMT pour la recherche de contre-exemples. La séance de cours se penche sur la vérification de type, la vérification de type bidirectionnelle et l'encodage des fonctionnalités de langage Scala. Il traite également de l'automatisation, des améliorations apportées à la vérification des programmes et des résultats théoriques de la recherche par contre-exemple. La présentation se termine par l'application de types dépendants, les transformations des programmes Scala et l'application des lois dans la conception des programmes.

À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.
Séances de cours associées (55)
Laboratoire de génération de code
Couvre la génération de code pour un compilateur, traduisant un programme Amy à WebAssembly, y compris la gestion de la mémoire et la compilation de correspondance de motifs.
Types de données C avancés
Couvre les types de données avancés et la gestion de la mémoire en programmation C, en mettant l'accent sur la cohérence des types et l'allocation dynamique des tableaux.
Hiérarchies de classe: Correspondance des motifs
Explore les hiérarchies de classe, les classes de cas, les enums, les correspondances de motifs et les valeurs de fonction dans Scala.
Fondements de Scala: Modélisation et Systèmes de Type
Couvre les fondements de Scala, y compris la modélisation des types récursifs, des types paramétrés et de la variance.
Laboratoire de vérification de type
Se concentre sur la mise en œuvre d'un vérificateur de type pour Amy, couvrant l'analyse des noms et des types, la génération de contraintes de frappe et l'importance de la vérification de type dans la compilation.
Afficher plus