Differences

This shows you the differences between two versions of the page.

--- apr:journees:ete2023 [2023/06/14 14:08]
mine [Programme]
+++ apr:journees:ete2023 [2023/06/14 14:08] (current)
mine [Résumés]
@@ Line 130: / Line 130: @@
-==== Résumés ====
-**Programmation à types dépendants avec Lean4**\\
-Frédéric Peschanski (APR, Sorbonne Université)\\
-D'après le site web de Lean4 - https://leanprover.github.io :
-> Lean est un langage de programmation fonctionnelle qui simplifie
-> la rédaction de programmes correctes et faciles à maintenir.
-> On peut également utiliser Lean4 comme un assistant de preuve.
-Ma présentation comportera principalement deux parties :
-Tout d'abord, je présenterai (assez superficiellement) les principes
-fondamentaux du langage, notamment le lambda-calcul à types dépendants
-et les types et familles inductives implémentées en Lean4.
-Dans la seconde partie, je présenterai des exemples de programmes
-qui mettent en pratique les types dépendants.
-----
-**Verifying a compiler for a synchronous dataflow language with state machines in Coq**\\
-Basile Pesin (PARKAS, Inria Paris)
-The Vélus project is a formalization of a synchronous block-diagram language, based on elements from Lustre and Scade 6, in the Coq interactive theorem prover.
-It includes a relational formalization of the dataflow semantics of the language, a compiler that uses the CompCert C compiler as a backend to produce assembly code, and an end-to-end proof that the dataflow semantics of the source program is preserved by the trace-based semantics of the generated assembly.
-Our recent work extends Vélus with higher-level constructs that are useful to define modal behaviors: switched blocks, shared variables (eg last x), reset blocks, and state machines.
-This talk will present this work, including the novel semantic model we developed to integrate these block-based constructions into the existing stream-based model.
-We will also show how we compile these constructs.
-We will outline the adaptations that must be done to the standard source-to-source rewriting schemes, and the invariants necessary to prove them correct in the context of an interactive theorem prover.
-Finally, we will explain how the backend of the compiler also needs to be adapted for efficient compilation of these constructs.
-----
-**Principal Geodesic Analysis of Merge Trees (and Persistence Diagrams)**\\
-Mathieu Pont (APR, SU)
-This paper presents a computational framework for the Principal Geodesic Analysis of merge trees (MT-PGA), a novel adaptation of the celebrated Principal Component Analysis (PCA) framework [87] to the Wasserstein metric space of merge trees [92]. We formulate MT-PGA computation as a constrained optimization problem, aiming at adjusting a basis of orthogonal geodesic axes, while minimizing a fitting energy. We introduce an efficient, iterative algorithm which exploits shared-memory parallelism, as well as an analytic expression of the fitting energy gradient, to ensure fast iterations. Our approach also trivially extends to extremum persistence diagrams. Extensive experiments on public ensembles demonstrate the efficiency of our approach - with MT-PGA computations in the orders of minutes for the largest examples. We show the utility of our contributions by extending to merge trees two typical PCA applications. First, we apply MT-PGA to data reduction and reliably compress merge trees by concisely representing them by their first coordinates in the MT-PGA basis. Second, we present a dimensionality reduction framework exploiting the first two directions of the MT-PGA basis to generate two-dimensional layouts of the ensemble. We augment these layouts with persistence correlation views, enabling global and local visual inspections of the feature variability in the ensemble. In both applications, quantitative experiments assess the relevance of our framework. Finally, we provide a C++ implementation that can be used to reproduce our results.
-----
-**Détection de contraintes de cardinalités**\\
-Marie Pelleau (Université Côte d’Azur)
-Les solveurs SAT sont utilisés avec succès dans de nombreuses applications combinatoires et du monde réel. Il n'est maintenant pas rare de lire qu’une preuve mathématique implique des centaines de gigaoctets de traces de solveur SAT. L'ampleur de la preuve commence à constituer une véritable limite à l'approche globale. Dans cette présentation, nous proposons de rechercher des contraintes de haut niveau dans les preuves UNSAT. Un travail similaire a été proposé il y a quelques années pour les contraintes de cardinalité les plus simples. Nous étendons cette idée à un cas plus général (sans limitation sur les bornes des contraintes de cardinalité) en généralisant l'algorithme de Bron & Kerbosh (pour l’énumération de cliques dans les graphes) aux hypergraphes.
-----
-**L'utilisation d'ACD dans la bibliothèque Spot**\\
-Alexandre Duretz-Lutz (EPITA)
-La décomposition en cycles alternante (ACD) est une structure qui montre
-l'imbrication des cycles acceptants et rejetants dans un ω-automate.
-Elle permet notamment de transformer un ω-automate avec condition
-d'acceptation quelconque en un automate à parité.  Nous discuterons de
-son utilisation dans Spot, initialement motivée par la nécessité de
-construire des automates à parité pour synthétiser des contrôleurs
-réactifs à partir de spécifications LTL.
-Cet exposé est une version étendue du papier "Practical applications of
-the Alternating Cycle Decomposition" présenté à TACAS'22 en
-collaboration avec Antonio Casares, Klara J. Meyer, Florian Renkin, et
-Salomon Sickert.
-----
-**Génération de générateur pour types contraints**\\
-Ghiles Ziat (EPITA)
-Il est fréquent de manipuler des valeurs numériques avec
-des contraintes non explicitées par leurs types. Par exemple, les
-intervalles d'entier sont des couples de nombres avec la
-contraintes que le premier (la borne inférieure) soit plus petit
-que le deuxième (borne supérieure). Un autre exemple est celui
-des arbres binaires de recherche ou les clés doivent etre
-rencontrées en ordre croissant lors d'un parcours en profondeur
-infixe. Nos travaux proposent de générer automatiquement des
-tests unitaires - à partir de la définition de ce genre de types
-- pour s'assurer que les contraintes associées au type ne sont
-pas violées par certaines fonctions. Pour générer ces tests, nous
-calculons, à l'aide de programmation par contrainte, une
-représentation de l'espace des habitants de ce type et enfin,
-nous générons le code du test qui générera aléatoirement et
-uniformément des habitants. Notre méthode est implémentée dans un
-prototype de pré-processeur pour OCaml appelé Testify.  Pour
-étendre notre méthode aux types récursifs, nous mixons de la
-génération de structures de données inductive à l'aide de la
-méthode de Boltzmann et la génération en domaines finis
-uniformément distribué en utilisant des contraintes globales.,
-Nous utilisons clp(fd) de SICStus Prolog comme bibliothèque de
-contraintes et la bibliothèque Arbogen en tant que générateur
-aléatoire de structures arborescentes.

Team APR

User Tools

Site Tools

Differences

Page Tools