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.

À 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 (32)

Concepts associés (50)

CS-550: Formal verification

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to u

Type (informatique)

vignette|Présentation des principaux types de données. En programmation informatique, un type de donnée, ou simplement un type, définit la nature des valeurs que peut prendre une donnée, ainsi que les opérateurs qui peuvent lui être appliqués. La plupart des langages de programmation de haut niveau offrent des types de base correspondant aux données qui peuvent être traitées directement — à savoir : sans conversion ou formatage préalable — par le processeur.

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.

Satisfiability modulo theories

En informatique et en logique mathématique, un problème de satisfiabilité modulo des théories (SMT) est un problème de décision pour des formules de logique du premier ordre avec égalité (sans quantificateurs), combinées à des théories dans lesquelles sont exprimées certains symboles de prédicat et/ou certaines fonctions. Des exemples de théories incluent la théorie des nombres réels, la théorie de l’arithmétique linéaire, des théories de diverses structures de données comme les listes, les tableaux ou les tableaux de bits, ainsi que des combinaisons de celles-ci.

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.

Terminal (informatique)

vignette|Un terminal DEC VT100. En informatique, un terminal est une variété de périphérique réseau placé à l'extrémité d'un nœud. Le terminal est un point d’accès de communication entre l'homme et un ordinateur central ou un réseau d'ordinateurs. Dans un réseau décentralisé de type client-serveur il correspond aujourd'hui à l'association minimale d'un périphérique de saisie (clavier) ou de pointage (souris) et d'un moniteur reliés à l'unité centrale.

Laboratoire de génération de code CS-320: Computer language processing

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.

Conception de l'amplificateur différentiel EE-320: Analog IC design

Couvre la conception d'un amplificateur différentiel avec des paramètres clés comme le gain et le courant de biais.

Types de données C avancés CS-207: System oriented programming

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.

Introduction à la programmation R pour la génétique et la génomique BIO-373: Genetics and genomics

Introduit un cours sur la génétique et la génomique, en se concentrant sur la programmation R avec des exercices interactifs.

Laboratoire de vérification de type CS-320: Computer language processing

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.