Séance de cours

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

Graph Chat

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

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.

Source officielle

Proximité ontologique

Informatique théorique

Théorie des langages de programmation: Langage de programmation de haut niveau

Concepts associés (32)

Type dépendant

En Informatique et en Logique, un type dépendant est un type qui peut dépendre d'une valeur définie dans le langage typé. Les langages Agda et Gallina (de l'assistant de preuve Coq) sont des exemples de langages à type dépendant. Les types dépendants permettent par exemple de définir le type des listes à n éléments. Voici un exemple en Coq. Inductive Vect (A: Type): nat -> Type := | nil: Vect A 0 | cons (n: nat) (x: A) (t: Vect A n): Vect A (S n).

Vérification formelle

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification can be helpful in proving the correctness of systems such as: cryptographic protocols, combinational circuits, digital circuits with internal memory, and software expressed as source code.

Type system

In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a type (for example, integer, floating point, string) to every "term" (a word, phrase, or other set of symbols). Usually the terms are various constructs of a computer program, such as variables, expressions, functions, or modules. A type system dictates the operations that can be performed on a term. For variables, the type system determines the allowed values of that term.

Bounds checking

In computer programming, bounds checking is any method of detecting whether a variable is within some bounds before it is used. It is usually used to ensure that a number fits into a given type (range checking), or that a variable being used as an array index is within the bounds of the array (index checking). A failed bounds check usually results in the generation of some sort of exception signal. As performing bounds checking during each use can be time-consuming, it is not always done.

Programmation fonctionnelle

La programmation fonctionnelle est un paradigme de programmation de type déclaratif qui considère le calcul en tant qu'évaluation de fonctions mathématiques. Comme le changement d'état et la mutation des données ne peuvent pas être représentés par des évaluations de fonctions la programmation fonctionnelle ne les admet pas, au contraire elle met en avant l'application des fonctions, contrairement au modèle de programmation impérative qui met en avant les changements d'état.

Afficher plus

Séances de cours associées (64)

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.

Compilateur de vérification: Approche Spec#

Explore le système de programmation Spec#, en se concentrant sur un compilateur de vérification pour C# 2.0.

Types dépendants dans les langages de programmation

Explore les cartes, les opérateurs de type, l'équivalence, les types de première classe, System Fw, Coq, et les défis de la vérification de type dans les langages de programmation.

Programmes de vérification avec l'inox: Comment fonctionne l'inox

Explore le fonctionnement intérieur du cadre Inox, en mettant l'accent sur les transformations de vérification et de contrôle de type dépendant.

Types dans Lambda Calculus

Couvre les types dans le calcul lambda, y compris la définition des types, la spécification des règles et la preuve de la solidité.

Afficher plus

Concepts associés (32)

Type dépendant

Vérification formelle

Type system

Bounds checking

Programmation fonctionnelle

Afficher plus