Séance de cours

Exactitude des compilateurs: Partie 2

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.

Dans cours

CS-320: Computer language processing

We teach the fundamental aspects of analyzing and interpreting computer languages, including the techniques to build compilers. You will build a working compiler from an elegant functional language into machine code using a popular backend called LLVM (htt ...

Description

Cette séance de cours se penche sur l'exactitude des compilateurs, en se concentrant sur l'interprétation des expressions et des opérations de pile. Il couvre l'évaluation des expressions, la compilation en bytecodes et l'exécution d'opérations sur une machine de pile. L'instructeur démontre le processus de vérification en utilisant Stainless, assurant l'exactitude des opérations du compilateur.

Enseignant·e

Viktor Kuncak

Viktor Kunčak joined EPFL in 2007, after receiving a PhD degree from MIT. Since then has been leading the Laboratory for Automated Reasoning and Analysis and supervised at least 12 completed PhD theses. His works on languages, algorithms and systems for verification and automated reasoning. He served as an initiator and one of the coordinators of a European network (COST action) in the area of automated reasoning, verification, and synthesis. In 2012 he received a 5-year single-investigator European Research Council (ERC) grant of 1.5M EUR. His invited talks include those at Lambda Days, Scala Days, NFM, LOPSTR, SYNT, ICALP, CSL, RV, VMCAI, and SMT. A paper on test generation he co-authored received an ACM SIGSOFT distinguished paper award at ICSE. A PLDI paper he co-authored was published in the Communications of the ACM as a Research Highlight article. His Google Scholar profile reports an over-approximate H-index of 38. He was an associate editor of ACM Transactions on Programming Languages and Systems (TOPLAS) and served as a co-chair of conferences on Computer-Aided Verification (CAV), Formal Methods in Computer Aided Design (FMCAD), Workshop on Synthesis (SYNT), and Verification, Model Checking, and Abstract Interpretation (VMCAI). At EPFL he teaches courses on functional and parallel programming, compilers, and verification. He has co-taught the MOOC "Parallel Programming" that was visited by over 100'000 learners and completed by thousands of students from all over the world.

Source officielle

Proximité ontologique

Informatique théorique

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

Concepts associés (30)

Expression (informatique)

Dans les langages de programmation, une expression est un élément de syntaxe qui combine un ensemble de lexèmes retournant une valeur. C'est une combinaison de littéraux, de variables, d'opérateurs, et de fonctions qui est évaluée (ou calculée) en suivant les règles de priorité et d'associativité du langage de programmation pour produire (ou retourner) une nouvelle valeur. Par exemple, 2+3 est une expression arithmétique qui vaut 5. Une variable est une expression car elle représente une valeur contenue en mémoire, donc y+6 est une expression.

Stratégie d'évaluation (informatique)

Un langage de programmation utilise une stratégie d'évaluation pour déterminer « quand » évaluer les arguments à l'appel d'une fonction (ou encore, opération, méthode) et « comment » passer les arguments à la fonction. Par exemple, dans l'appel par valeur, les arguments doivent être évalués avant d'être passés à la fonction. La stratégie d'évaluation d'un langage de programmation est spécifiée par la définition du langage même. En pratique, la plupart des langages de programmation (Java, C...

Évaluation paresseuse

L’évaluation paresseuse (), appelée aussi appel par nécessité ou évaluation retardée est une technique d'implémentation des programmes récursifs pour laquelle l'évaluation d'un paramètre de fonction ne se fait pas avant que les résultats de cette évaluation ne soient réellement nécessaires. Ces résultats, une fois calculés, sont préservés pour des réutilisations ultérieures. Dans un langage comme Haskell, l'évaluation est paresseuse par défaut.

Short-circuit evaluation

Short-circuit evaluation, minimal evaluation, or McCarthy evaluation (after John McCarthy) is the semantics of some Boolean operators in some programming languages in which the second argument is executed or evaluated only if the first argument does not suffice to determine the value of the expression: when the first argument of the AND function evaluates to false, the overall value must be false; and when the first argument of the OR function evaluates to true, the overall value must be true.

F Sharp

F# est un langage de programmation fonctionnel, impératif et orienté objet pour la plate-forme .NET. F# est développé par Microsoft Research et son noyau est dérivé du langage OCaml, avec lequel il est fortement compatible. Ces deux langages de programmation font partie de la même famille que les langages ML. Ce langage a été conçu spécifiquement pour la plate-forme .NET, donc fortement orienté-objet. Depuis novembre 2010, Microsoft a mis à la disposition de tous les bibliothèques core et son compilateur F#, sous la licence Apache 2.

Afficher plus

Séances de cours associées (32)

Préfixe, Infix, Postfix et génération de code

Explore les notations de préfixe, d'infixe et de postfixe dans les expressions et leur rôle dans la génération de code.

Introduction au traitement du langage informatique

Couvre le traitement du langage informatique, les compilateurs, les compétences acquises et des exemples d'application.

La CEPA et le bug

Explore la CEPA, les compilateurs et l'origine du terme «bug» dans l'informatique.

Compilateurs : défis avec les processeurs de signaux numériques

Couvre les défis de la compilation pour les processeurs de signaux numériques en raison de leurs caractéristiques architecturales uniques et des irrégularités.

Vérification des compilateurs : défis et avantages

Examine les défis et les avantages de la vérification des compilateurs, en soulignant l'importance de la vérification des compilateurs pour les logiciels critiques.

Afficher plus

Concepts associés (30)

Expression (informatique)

Stratégie d'évaluation (informatique)

Évaluation paresseuse

Short-circuit evaluation

F Sharp

Afficher plus