CINXE.COM

<!DOCTYPE html> <html xmlns="http://www.w3.org/1999/xhtml" lang="fr" dir="ltr" class="no-js"> <head> <meta charset="UTF-8" /> <title>Bienvenue</title>  <script> var _paq = window._paq = window._paq || []; /* tracker methods like "setCustomDimension" should be called before "trackPageView" */ _paq.push(['trackPageView']); _paq.push(['enableLinkTracking']); (function() { var u="//apps.roulois.fr/matomo/"; _paq.push(['setTrackerUrl', u+'matomo.php']); _paq.push(['setSiteId', '1']); var d=document, g=d.createElement('script'), s=d.getElementsByTagName('script')[0]; g.async=true; g.src=u+'matomo.js'; s.parentNode.insertBefore(g,s); })(); </script>  <script>(function(H){H.className=H.className.replace(/\bno-js\b/,'js')})(document.documentElement)</script> <meta name="viewport" content="width=device-width,initial-scale=1" /> <link rel="shortcut icon" href="https://www.irif.fr/_media/favicon.ico" /> <link rel="apple-touch-icon" href="https://www.irif.fr/_media/apple-touch-icon.png" /> <meta name="generator" content="DokuWiki"/> <meta name="robots" content="index,follow"/> <meta name="keywords" content="index"/> <link rel="search" type="application/opensearchdescription+xml" href="https://www.irif.fr/lib/exe/opensearch.php" title=""/> <link rel="start" href="https://www.irif.fr/"/> <link rel="contents" href="https://www.irif.fr/index?do=index" title="Plan du site"/> <link rel="manifest" href="https://www.irif.fr/lib/exe/manifest.php"/> <link rel="alternate" type="text/html" title="HTML brut" href="https://www.irif.fr/_export/xhtml/index"/> <link rel="alternate" type="text/plain" title="Wiki balise" href="https://www.irif.fr/_export/raw/index"/> <link rel="canonical" href="https://www.irif.fr/"/> <link rel="stylesheet" href="https://www.irif.fr/lib/exe/css.php?t=bootstrap3&tseed=999b1f07158911a883ed4b945a522775"/> <link type="text/css" rel="stylesheet" href="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net-fixedheader-dt/css/fixedHeader.dataTables.min.css"/> <link type="text/css" rel="stylesheet" href="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net-fixedcolumns-dt/css/fixedColumns.dataTables.min.css"/> <link type="text/css" rel="stylesheet" href="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net/css/dataTables.bootstrap.min.css"/> <link type="text/css" rel="stylesheet" href="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net-buttons/css/buttons.bootstrap.min.css"/> <link type="text/css" rel="stylesheet" href="https://www.irif.fr/lib/plugins/icons/assets/font-awesome/css/font-awesome.min.css"/> <link type="text/css" rel="stylesheet" href="https://www.irif.fr/lib/plugins/icons/assets/material-design-icons/css/materialdesignicons.min.css"/>  <script >/*<![CDATA[*/var NS='';var JSINFO = {"plugin":{"datatables":{"config":{"dom":"lBfrtip","language":{"url":"https:\/\/www.irif.fr\/lib\/plugins\/datatables\/assets\/datatables.net-i18n\/fr-FR.json"}},"enableForAllTables":1}},"move_renameokay":false,"move_allowrename":false,"bootstrap3":{"mode":"show","toc":[],"config":{"collapsibleSections":0,"fixedTopNavbar":1,"showSemanticPopup":0,"sidebarOnNavbar":1,"tagsOnTop":1,"tocAffix":1,"tocCollapseOnScroll":1,"tocCollapsed":0,"tocLayout":"default","useAnchorJS":1,"useAlternativeToolbarIcons":1}},"id":"index","namespace":"","ACT":"show","useHeadingNavigation":1,"useHeadingContent":1}; /*!]]>*/</script> <script src="https://www.irif.fr/lib/exe/jquery.php?tseed=34a552433bc33cc9c3bc32527289a0b2" defer="defer"></script> <script src="https://www.irif.fr/lib/exe/js.php?t=bootstrap3&tseed=999b1f07158911a883ed4b945a522775" defer="defer"></script> <script type="text/javascript" src="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net/js/jquery.dataTables.min.js" defer="defer"></script> <script type="text/javascript" src="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net-fixedheader-dt/js/fixedHeader.dataTables.min.js" defer="defer"></script> <script type="text/javascript" src="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net-fixedcolumns-dt/js/fixedColumns.dataTables.min.js" defer="defer"></script> <script type="text/javascript" src="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net-buttons/js/dataTables.buttons.min.js" defer="defer"></script> <script type="text/javascript" src="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net-buttons/js/buttons.html5.min.js" defer="defer"></script> <script type="text/javascript" src="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net-buttons/js/buttons.print.min.js" defer="defer"></script> <script type="text/javascript" src="https://www.irif.fr/lib/plugins/datatables/assets/jszip/jszip.min.js" defer="defer"></script> <script type="text/javascript" src="https://www.irif.fr/lib/plugins/datatables/assets/pdfmake/pdfmake.min.js" defer="defer"></script> <script type="text/javascript" src="https://www.irif.fr/lib/plugins/datatables/assets/pdfmake/vfs_fonts.js" defer="defer"></script> <script type="text/javascript" src="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net/js/dataTables.bootstrap.min.js" defer="defer"></script> <script type="text/javascript" src="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net-buttons/js/buttons.bootstrap.min.js" defer="defer"></script> <script type="text/x-mathjax-config">/*<![CDATA[*/MathJax.Hub.Config({ tex2jax: { inlineMath: [ ["$","$"], ["\$","\$"] ], displayMath: [ ["$$","$$"], ["\\[","\\]"] ], processEscapes: true } }); /*!]]>*/</script> <script type="text/javascript" charset="utf-8" src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.9/MathJax.js?config=TeX-AMS_CHTML.js"></script>  <style type="text/css">@media screen { body { margin-top: 60px; } #dw__toc.affix { top: 50px; position: fixed !important; } #dw__toc .nav .nav .nav { display: none; } }</style>  </head> <body class="simplex dokuwiki mode_show tpl_bootstrap3 home dw-fluid-container" data-page-id="index"><div class="dokuwiki"> <header id="dokuwiki__header" class="dw-container dokuwiki container-fluid mx-5">  <nav id="dw__navbar" class="navbar navbar-fixed-top navbar-inverse" role="navigation"> <div class="dw-container container-fluid mx-5"> <div class="navbar-header"> <button class="navbar-toggle" type="button" data-toggle="collapse" data-target=".navbar-collapse"> <span class="icon-bar"></span> <span class="icon-bar"></span> <span class="icon-bar"></span> </button> <a class="navbar-brand d-flex align-items-center" href="https://www.irif.fr/index" accesskey="h" title=""><img id="dw__logo" class="pull-left h-100 mr-4" alt="" src="https://www.irif.fr/_media/logo.png" /><div class="pull-right"><div id="dw__title"></div></div></a> </div> <div class="collapse navbar-collapse"> <ul class="nav navbar-nav"> <li class="level1 node dropdown"><a href="#" class="dropdown-toggle" data-target="#" data-toggle="dropdown" role="button" aria-haspopup="true" aria-expanded="false">INFORMATIONS <span class="caret"></span></a> <ul class="dropdown-menu" role="menu"> <li class="level2"> <a href="https://www.irif.fr/informations/presentation" class="wikilink1" title="informations:presentation" >Présentation</a> </li> <li class="level2"> <a href="https://www.irif.fr/informations/contacts" class="wikilink1" title="informations:contacts" >Contacts et accès</a> </li> <li class="level2"> <a href="https://www.irif.fr/informations/charte" class="wikilink1" title="informations:charte" >Charte des membres de l’IRIF</a> </li> <li class="level2"> <a href="https://www.irif.fr/egalite-fh/index" class="wikilink1" title="egalite-fh:index" >Égalités</a> </li> <li class="level2"> <a href="https://www.irif.fr/environnement/index" class="wikilink1" title="environnement:index" >Environment</a> </li> <li class="level2"> <a href="https://www.irif.fr/informations/annuaire" class="wikilink1" title="informations:annuaire" >Annuaire</a> </li> <li class="level2"> <a href="https://www.irif.fr/informations/mentorat" class="wikilink1" title="informations:mentorat" >Programme de mentorat</a> </li> <li class="level2"> <a href="https://www.irif.fr/informations/childcare" class="wikilink1" title="informations:childcare" >Childcare program</a> </li> <li class="level2"> <a href="https://www.irif.fr/informations/hceres" class="wikilink1" title="informations:hceres" >Évaluation HCERES - 28 au 30 Novembre 2023 (vague D)</a> </li> </ul> </li> </ul> <ul class="nav navbar-nav"> <li class="level1 node dropdown"><a href="#" class="dropdown-toggle" data-target="#" data-toggle="dropdown" role="button" aria-haspopup="true" aria-expanded="false">RECHERCHE <span class="caret"></span></a> <ul class="dropdown-menu" role="menu"> <li class="level2"> <strong><a href="https://www.irif.fr/poles/asd/index" class="wikilink1" title="poles:asd:index" >Algorithmes et structures discrètes</a></strong> </li> <li class="level2"> <a href="https://www.irif.fr/equipes/algocomp/index" class="wikilink1" title="equipes:algocomp:index" >Algorithmes et complexité</a> </li> <li class="level2"> <a href="https://www.irif.fr/equipes/distribue/index" class="wikilink1" title="equipes:distribue:index" >Calcul distribué</a> </li> <li class="level2"> <a href="https://www.irif.fr/equipes/combi/index" class="wikilink1" title="equipes:combi:index" >Combinatoire</a> </li> <li class="level2"> <a href="https://www.irif.fr/equipes/graphes/index" class="wikilink1" title="equipes:graphes:index" >Théorie et algorithmique des graphes</a> </li> <li class="level2"> <strong><a href="https://www.irif.fr/poles/asv/index" class="wikilink1" title="poles:asv:index" >Automates, structures et vérification</a></strong> </li> <li class="level2"> <a href="https://www.irif.fr/equipes/automates/index" class="wikilink1" title="equipes:automates:index" >Automates et applications</a> </li> <li class="level2"> <a href="https://www.irif.fr/equipes/verif/index" class="wikilink1" title="equipes:verif:index" >Modélisation et vérification</a> </li> <li class="level2"> <strong><a href="https://www.irif.fr/poles/pps/index" class="wikilink1" title="poles:pps:index" >Preuves, programmes et systèmes</a></strong> </li> <li class="level2"> <a href="https://www.irif.fr/equipes/algebre/index" class="wikilink1" title="equipes:algebre:index" >Algèbre et calcul</a> </li> <li class="level2"> <a href="https://www.irif.fr/equipes/programmes/index" class="wikilink1" title="equipes:programmes:index" >Programmes et Langages (PL)</a> </li> <li class="level2"> <a href="https://www.irif.fr/equipes/preuves/index" class="wikilink1" title="equipes:preuves:index" >Preuves et programmes</a> </li> <li class="level2"> <a href="https://www.irif.fr/equipes/picube/index" class="wikilink1" title="equipes:picube:index" >Picube (Inria)</a> <hr/> </li> <li class="level2"> <strong><a href="https://cnrs.hal.science/IRIF/" class="" title="https://cnrs.hal.science/IRIF/" rel="ugc nofollow">PUBLICATIONS (hal)</a></strong> </li> </ul> </li> </ul> <ul class="nav navbar-nav"> <li class="level1 node dropdown"><a href="#" class="dropdown-toggle" data-target="#" data-toggle="dropdown" role="button" aria-haspopup="true" aria-expanded="false">ÉVÉNEMENTS <span class="caret"></span></a> <ul class="dropdown-menu" role="menu"> <li class="level2"> <strong><a href="https://www.irif.fr/seminaires/evenements" class="wikilink1" title="seminaires:evenements" >Evénements de l'IRIF</a></strong> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/irif/index" class="wikilink1" title="seminaires:irif:index" >IRIF Distinguished Talks Series</a> </li> <li class="level2"> <a href="https://www.irif.fr/rencontres/irif/index" class="wikilink1" title="rencontres:irif:index" >Journées de l'IRIF</a> </li> <li class="level2"> <a href="https://www.irif.fr/rencontres/poles/index" class="wikilink1" title="rencontres:poles:index" >Rencontres de pôles</a> </li> <li class="level2"> <strong><a href="https://www.irif.fr/seminaires/seminaires" class="wikilink1" title="seminaires:seminaires" >Séminaires de recherche</a></strong> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/algocomp/index" class="wikilink1" title="seminaires:algocomp:index" >Algorithmes et complexité</a> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/asd/index" class="wikilink1" title="seminaires:asd:index" >Algorithmes et structures discrètes</a> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/automates/index" class="wikilink1" title="seminaires:automates:index" >Automates</a> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/combi/index" class="wikilink1" title="seminaires:combi:index" >Combinatoire énumérative et analytique</a> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/picube/index" class="wikilink1" title="seminaires:picube:index" >Séminaire Formath (Formalized Mathematics)</a> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/adg/index" class="wikilink1" title="seminaires:adg:index" >Graphes et calcul distribué</a> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/pps/index" class="wikilink1" title="seminaires:pps:index" >Preuves, programmes et systèmes</a> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/verif/index" class="wikilink1" title="seminaires:verif:index" >Vérification</a> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/doctorants/index" class="wikilink1" title="seminaires:doctorants:index" >Séminaire des membres non-permanents</a> </li> <li class="level2"> <strong><a href="https://www.irif.fr/seminaires/onlineseminars" class="wikilink1" title="seminaires:onlineseminars" >Séminaires en ligne</a></strong> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/greta/index" class="wikilink1" title="seminaires:greta:index" >Graph Transformation Theory and Applications</a> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/numeration/index" class="wikilink1" title="seminaires:numeration:index" >One world numeration seminar</a> </li> <li class="level2"> <strong><a href="https://www.irif.fr/seminaires/gt" class="wikilink1" title="seminaires:gt" >Groupes de travail</a></strong> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/cat/index" class="wikilink1" title="seminaires:cat:index" >Catégories supérieures, polygraphes et homotopie</a> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/sms/index" class="wikilink1" title="seminaires:sms:index" >La syntaxe rencontre la sémantique</a> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/hott/index" class="wikilink1" title="seminaires:hott:index" >La théorie des types et la théorie de l'homotopie</a> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/laag/index" class="wikilink1" title="seminaires:laag:index" >Logique, automates, algèbre et jeux</a> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/programmation/index" class="wikilink1" title="seminaires:programmation:index" >Programmation</a> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/semantique/index" class="wikilink1" title="seminaires:semantique:index" >Sémantique</a> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/types/index" class="wikilink1" title="seminaires:types:index" >Théorie des types et réalisabilité</a> </li> <li class="level2"> <strong><a href="https://www.irif.fr/seminaires/soutenances" class="wikilink1" title="seminaires:soutenances" >Soutenances</a></strong> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/these/index" class="wikilink1" title="seminaires:these:index" >Soutenances de thèses</a> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/hdr/index" class="wikilink1" title="seminaires:hdr:index" >Soutenances d'habilitation</a> </li> </ul> </li> </ul> <ul class="nav navbar-nav"> <li class="level1 node dropdown"><a href="#" class="dropdown-toggle" data-target="#" data-toggle="dropdown" role="button" aria-haspopup="true" aria-expanded="false">MÉDIATION <span class="caret"></span></a> <ul class="dropdown-menu" role="menu"> <li class="level2"> <a href="https://www.irif.fr/mediation/fdls" class="wikilink1" title="mediation:fdls" >Fête de la Science</a> </li> <li class="level2"> <a href="https://www.irif.fr/mediation/confcrypto" class="wikilink1" title="mediation:confcrypto" >Conférence vidéo “Manuel de Cryptanalyse à l’usage de la NSA”</a> </li> <li class="level2"> <a href="https://www.irif.fr/mediation/scolaire" class="wikilink1" title="mediation:scolaire" >Stages scolaires d’observation</a> </li> <li class="level2"> <a href="https://www.irif.fr/portraits/index" class="wikilink1" title="portraits:index" >Portraits de recherche</a> </li> <li class="level2"> <a href="https://icalp2022.irif.fr/?page_id=1111" class="" title="https://icalp2022.irif.fr/?page_id=1111" rel="ugc nofollow">Exposition 50 ans</a> </li> <li class="level2"> <a href="https://qubobs.irif.fr/fr/" class="" title="https://qubobs.irif.fr/fr/" rel="ugc nofollow">Projet QuBOBS (quantum computing explained)</a> </li> </ul> </li> </ul> <ul class="nav navbar-nav"> <li class="level1 node dropdown"><a href="#" class="dropdown-toggle" data-target="#" data-toggle="dropdown" role="button" aria-haspopup="true" aria-expanded="false">POINTS CLÉS <span class="caret"></span></a> <ul class="dropdown-menu" role="menu"> <li class="level2"> <a href="https://www.irif.fr/distinctions/index" class="wikilink1" title="distinctions:index" > Prix et distinctions</a> </li> <li class="level2"> <a href="https://www.irif.fr/logiciels/index" class="wikilink1" title="logiciels:index" >Logiciels</a> </li> <li class="level2"> <a href="https://www.irif.fr/contrats/index" class="wikilink1" title="contrats:index" >Contrats</a> </li> <li class="level2"> <a href="https://www.irif.fr/international/index" class="wikilink1" title="international:index" >Collaborations internationales</a> </li> <li class="level2"> <a href="https://epit.irif.fr" class="" title="https://epit.irif.fr" rel="ugc nofollow">L'école thématique EPIT</a> </li> <li class="level2"> <a href="https://www.irif.fr/formation/index" class="wikilink1" title="formation:index" >Formation</a> </li> </ul> </li> </ul> <ul class="nav navbar-nav"> <li class="level1 node dropdown"><a href="#" class="dropdown-toggle" data-target="#" data-toggle="dropdown" role="button" aria-haspopup="true" aria-expanded="false">REJOIGNEZ-NOUS <span class="caret"></span></a> <ul class="dropdown-menu" role="menu"> <li class="level2"> <a href="https://www.irif.fr/informations/visit" class="wikilink1" title="informations:visit" >Programme visiteurs</a> </li> <li class="level2"> <a href="https://www.irif.fr/postes/admin" class="wikilink1" title="postes:admin" >Postes soutien à la recherche</a> </li> <li class="level2"> <a href="https://www.irif.fr/postes/universite" class="wikilink1" title="postes:universite" >Enseignant·e·s-chercheurs·euses</a> </li> <li class="level2"> <a href="https://www.irif.fr/postes/chercheur" class="wikilink1" title="postes:chercheur" >Chercheurs·euses</a> </li> <li class="level2"> <a href="https://www.irif.fr/postes/postdoc" class="wikilink1" title="postes:postdoc" >Postdocs</a> </li> <li class="level2"> <a href="https://www.irif.fr/postes/ater" class="wikilink1" title="postes:ater" >ATER</a> </li> <li class="level2"> <a href="https://www.irif.fr/postes/these" class="wikilink1" title="postes:these" >Thèses</a> </li> <li class="level2"> <a href="https://www.irif.fr/postes/stage" class="wikilink1" title="postes:stage" >Stages de master</a> </li> <li class="level2"> <a href="https://www.irif.fr/postes/stage-scolaire" class="wikilink1" title="postes:stage-scolaire" >Stages scolaires d’observation</a> </li> </ul> </li> </ul> <ul class="nav navbar-nav"> <li class="level1"> <a href="https://www.irif.fr/intranet/index" class="wikilink1" title="intranet:index" >INTRANET</a> </li> </ul> <div class="navbar-right" id="dw__navbar_items">  <ul class="nav navbar-nav" id="dw__translation"> <li class="dropdown"> <a href="" class="dropdown-toggle" data-target="#" data-toggle="dropdown" title="Traductions de cette page" role="button" aria-haspopup="true" aria-expanded="false"> <span class="iconify" data-icon="mdi:flag"></span> <span class="hidden-lg hidden-md hidden-sm">Traductions de cette page</span><span class="caret"></span> </a> <ul class="dropdown-menu" role="menu"> <li class="dropdown-header hidden-xs hidden-sm"> <span class="iconify" data-icon="mdi:flag"></span> Traductions de cette page </li> <li><div class='li cur'><a href="https://www.irif.fr/index" class="wikilink1 cur flag" title="Français"><img src="https://www.irif.fr/lib/plugins/translation/flags/fr.gif" alt="fr" height="11" />Français</a></li><li><div class='li'><a href="https://www.irif.fr/en/index" class="wikilink1 flag" title="English"><img src="https://www.irif.fr/lib/plugins/translation/flags/en.gif" alt="en" height="11" />English</a></li> </ul> </li> </ul>  <ul class="nav navbar-nav"> <li> <span class="dw__actions dw-action-icon"> <a href="https://www.irif.fr/index?do=login&sectok=" title="S'identifier" rel="nofollow" class="menuitem login btn btn-default navbar-btn"><svg xmlns="http://www.w3.org/2000/svg" width="24" height="24" viewBox="0 0 24 24"><path d="M10 17.25V14H3v-4h7V6.75L15.25 12 10 17.25M8 2h9a2 2 0 0 1 2 2v16a2 2 0 0 1-2 2H8a2 2 0 0 1-2-2v-4h2v4h9V4H8v4H6V4a2 2 0 0 1 2-2z"/></svg><span class=""> S'identifier</span></a> </span> </li> </ul> </div> </div> </div> </nav>  </header> <a name="dokuwiki__top" id="dokuwiki__top"></a> <main role="main" class="dw-container pb-5 dokuwiki container-fluid mx-5"> <div id="dokuwiki__pageheader"> <p class="text-right"> </p> <div id="dw__msgarea" class="small"> </div> </div> <div class="row"> <article id="dokuwiki__content" class="col-sm-12 col-md-12 " itemscope itemtype="http://schema.org/Article" itemref="dw__license">  <div class="no-panel" itemprop="articleBody"> <div class="page "> <div class="dw-content-page "><div class="dw-content"><div class="plugin_include_content plugin_include__bandeau" id="plugin_include__bandeau"> <p> <em> </p> <div class="group plugin_wrap"><div class="wrap_column plugin_wrap" style="width: 40%;"> <p> <a href="https://www.irif.fr" class="media" title="https://www.irif.fr" rel="ugc nofollow"><img src="https://www.irif.fr/_media/irif_horizontal_noborder.svg" class="mediaright img-responsive" loading="lazy" title="Institut de Recherche en Informatique Fondamentale (IRIF)" alt="Institut de Recherche en Informatique Fondamentale (IRIF)" /></a> </p> </div><div class="wrap_right wrap_column plugin_wrap" style="width: 7%;"> <p> <a href="https://www.cnrs.fr" class="media" title="https://www.cnrs.fr" rel="ugc nofollow"><img src="https://www.irif.fr/_media/logocnrsnoir.svg" class="medialeft img-responsive" loading="lazy" title="CNRS" alt="CNRS" /></a> </p> </div><div class="wrap_right wrap_column plugin_wrap" style="width: 7%;"> <p> <a href="https://www.u-paris.fr" class="media" title="https://www.u-paris.fr" rel="ugc nofollow"><img src="https://www.irif.fr/_media/logoupnoir.svg" class="mediaright img-responsive" loading="lazy" title="Université Paris Cité" alt="Université Paris Cité" /></a> </p> </div><div class="wrap_clear plugin_wrap"></div></div> <p> </em> </p> <div class="plugin_wrap"> <p> <img src="https://www.irif.fr/_media/sophie_germain_extrathin.jpg" class="mediacenter img-responsive" loading="lazy" alt="" /> </p> </div></div> <div class="group plugin_wrap"><div class="wrap_column wrap_third plugin_wrap"> <h2 class="sectionedit17 page-header pb-3 mb-4 mt-5" id="bienvenue">Bienvenue</h2> <div class="plugin_include_content plugin_include__bienvenue" id="plugin_include__bienvenue"> <div class="level0"> <p> L'IRIF est une unité mixte de recherche (UMR 8243) entre le <a href="http://www.cnrs.fr" class="urlextern" title="http://www.cnrs.fr" rel="ugc nofollow">CNRS</a> et l'<a href="http://www.u-paris.fr/" class="urlextern" title="http://www.u-paris.fr/" rel="ugc nofollow">Université Paris Cité</a>, et héberge une équipe-projet <a href="http://www.inria.fr" class="urlextern" title="http://www.inria.fr" rel="ugc nofollow">Inria</a>. </p> <p> Les recherches menées à l'IRIF reposent sur l’étude et la compréhension des fondements de toute l’informatique, afin d’apporter des solutions innovantes aux défis actuels et futurs des sciences numériques.<br/> </p> <p> L'IRIF regroupe près de deux cents personnes. Sept de ses membres ont été lauréats de l'<a href="https://erc.europa.eu" class="urlextern" title="https://erc.europa.eu" rel="ugc nofollow">European Research Council (ERC)</a>, trois sont membres de l'<a href="http://www.iufrance.fr" class="urlextern" title="http://www.iufrance.fr" rel="ugc nofollow">Institut Universitaire de France (IUF)</a>, deux sont membres de l'<a href="http://www.ae-info.org" class="urlextern" title="http://www.ae-info.org" rel="ugc nofollow">Academia Europæa</a>, et un est membre de l'<a href="https://www.academie-sciences.fr/" class="urlextern" title="https://www.academie-sciences.fr/" rel="ugc nofollow">Académie des sciences</a>. </p> </div> </div> <h2 class="sectionedit20 page-header pb-3 mb-4 mt-5" id="notion_du_jour">Notion du jour</h2> <div class="plugin_include_content plugin_include__actualites:notion" id="plugin_include__actualites__notion"> <p> <div id="quote"></div> <script> var seed = 6; seededRandom = function(max) { seed = seed % 233280; seed = (seed * 9301 + 49297) % 233280; seed = (seed * 9301 + 49297) % 233280; seed = (seed * 9301 + 49297) % 233280; seed = (seed * 9301 + 49297) % 233280; return seed % max; } var quotes = [ // in order to select the first news (or another), set index =0 at the end (or another number) { text: "A <b>Young tableau</b> is a combinatorial object introduced by Alfred Young, a mathematician at Cambridge University, in 1900. It provides a convenient way to describe the group representations of the symmetric and general linear groups and to study their properties. A Young diagram is a finite collection of boxes, or cells, arranged in left-justified rows, with the row lengths in non-increasing order. A Young tableau is obtained by filling in the boxes of the Young diagram with numbers. Young tableaux have numerous applications in combinatorics, representation theory, and algebraic geometry.", img: "https://www.irif.fr/_media/actualites/2560px-young_tableaux_for_541_partition.svg.png" }, { text: "A function is <b>polymorphic</b> when it can be applied to arguments of different types. For instance, the identity function <i>fun x = x</i> is polymorphic since it can be applied, say, to integers and Boolean arguments, while the successor function <i>fun x = x+1</i> is not, since it can be applied only to integers. The latter function has type <i>Int→Int</i>, while the former has type ∀α.α→α, that is, it has type α→α for all possibles types α. The last type is a <b>polymorphic type</b>. <b>Set theoretic types</b> are types with union, intersection, and negation connectives: again <i>fun x = x</i> has both type <i>Int→Int</i> and <i>Bool→Bool</i> and, thus, it has the intersection type (<i>Int→Int</i>)∩(<i>Bool→Bool</i>).", img: "https://cdn-icons-png.flaticon.com/512/3064/3064095.png" }, { text: "<b>Backpropagation</b> (backward propagation of errors) is an algorithm for supervised learning of multilayer neural networks using gradient descent. One major problem in training those networks is in deciding how to learn good internal representations. Since internal nodes have no target output, any error function for that nodes will be dependent on the values of the parameters in the previous and following layers. Backpropagation simplifies the mathematics of gradient descent, while also facilitating its efficient calculation.", img: "https://cdn-icons-png.flaticon.com/512/2103/2103718.png" }, { text: "<b>Software verification</b> is a discipline of software engineering whose goal is to assure that software fully satisfies all the expected requirements. There are two fundamental approaches to verification: dynamic verification (or testing) and static verification (or analysis). Dynamic verification is performed during the execution of software, and dynamically checks its behavior. Static verification is the process of checking that software meets requirements by inspecting the code before it runs.", img: "https://cdn-icons-png.flaticon.com/512/1328/1328821.png" }, { text: "In computer science, <b>model checking</b> is exhaustively and automatically checking whether the mathematical model of some given system meets a given specification. Typically, one has hardware or software systems in mind, whereas the specification contains safety requirements such as the absence critical states that can cause the system to crash. To this end, the problem is formulated as an algorithmic task in logic, namely to check whether a given structure satisfies a given logical formula. This general concept applies to many kinds of logic and suitable structures. An important class of model checking methods have been developed for checking models of hardware and software designs where the specification is given by a temporal logic formula.", img: "https://cdn-icons-png.flaticon.com/512/1518/1518610.png" }, { text: "<b>Descriptive complexity</b> is a branch of computational complexity theory and of finite model theory that characterizes complexity classes by the type of logic needed to express the languages in them. For example, the polynomial hierarchy is precisely the class of languages expressible by statements of second-order logic. This connection between complexity and the logic of finite structures allows results to be transferred easily from one area to the other, facilitating new proof methods. The first main result of descriptive complexity was Fagin's theorem (1974). It established that NP is precisely the set of languages expressible by sentences of existential second-order logic. Many other classes were later characterized in such a manner.", img: "https://cdn-icons-png.flaticon.com/512/1356/1356321.png" }, { text: "<b>Computational complexity</b> theory focuses on classifying computational problems according to their inherent difficulty, and relating these classes to each other. A problem is regarded as inherently difficult if its solution requires significant resources, whatever the algorithm used. The ressources are usually time and storage, but can also be, for instance, the amount of communication, the number of gates in a circuit and the number of processors. One of the roles of computational complexity theory is to determine the practical limits on what computers can and cannot do. The P versus NP problem, one of the seven Millennium Prize Problems, is dedicated to the field of computational complexity.", img: "https://cdn-icons-png.flaticon.com/512/1584/1584892.png" }, { text: "<b>Linear logic</b>, a refinement of classical and intuitionistic logic, was introduced by Jean-Yves Girard in 1987 as a logic of actions and resources enabling one to describe dynamics of processes and resource handling. Ideas from linear logic have been influential in fields such as programming languages, game semantics, quantum physics, and linguistics. Given its focus on resources, linear logic has found many applications in Computer Science.", img: "https://img.icons8.com/ios-filled/2x/artificial-intelligence.png" }, { text: "The <b>sensitivity conjecture</b> relates to Boolean functions, which maps string of bits into a single output bit. They play an important role in complexity theory, as well in the design of circuits and chips for digital computers. There are many complexity measures of a Boolean function and almost all of them are known to be polynomially related. However, until July 2019, there was one unknown case, the so-called sensitivity of a boolean function, which measures how sensitive the function is when changing one input at a time. In 1992, Noam Nisan and Mario Szegedy conjectured that the sensitivity is also polynomially related to the other measures. In July 2019, Huang developed an algebraic method for proving the conjecture.", img: "https://cdn-icons-png.flaticon.com/512/38/38961.png" }, { text: "<b>Session types</b> can be thought of as “types for protocols”, insofar as they describe all the possible sequences of interactions between services, together with the type of the information exchanged in these interactions. Programs can be checked to see if the processes they implement conform to the protocols described by a session type.", img: "https://cdn-icons-png.flaticon.com/512/1122/1122581.png" }, { text: "A <b>formal system</b> is used to infer theorems from axioms according to a set of rules. These rules used to carry out the inference of theorems from axioms are known as the logical calculus of the formal system. In 1921, David Hilbert proposed to use such system as the foundation for the knowledge in mathematics. There are several properties that a formal system may have, including completeness, consistency, and the existence of an effective axiomatization. The incompleteness theorems, pioneered by Gödel, show that systems which contain a sufficient amount of arithmetic cannot possess all three of these properties.", img: "https://upload.wikimedia.org/wikipedia/commons/thumb/7/7c/Logic_portal.svg/1280px-Logic_portal.svg.png" }, { text: "A <b>parity game</b> is played on a colored directed graph, where each node has been colored by a priority. Two players, 0 and 1, move alternatively a token along the edges of the graph. The winner of a finite play is the player whose opponent is unable to move. In an infinite play, player 0 wins if the largest priority that occurs infinitely often in the play is even. Player 1 wins otherwise. Deciding which of the two players has a winning strategy is in NP and Co-NP, but can be solved in quasipolynomial time. Parity game solving can be seen as the algorithmic backend to problems in automated verification and controller synthesis.", img: "https://cdn-icons-png.flaticon.com/512/5525/5525472.png" }, { text: "<b>Virtual machines</b> (VMs) are a software abstraction of a whole computational system. VMs are mainly used to simulate hardware architectures which are not physically available, or to run multiple guest machines on a single hardware. Among the advantages, it is possible to decrease the total cost of ownership of an IT infrastructure, reach high availability, better compartmentalize systems to improve resilience and fault tolerance.", img: "https://www.pinclipart.com/picdir/big/95-954608_the-virtual-machine-has-two-frames-with-one.png" }, { text: "<b>Call-By-Push-Value</b> (CBPV) is a theoretical programming language discovered by Paul Blain Levy. It classifies programs into two distinct syntactic classes, inert results called <i>values</i> and active processes called <i>computations</i>. Intuitively, a value is, a computation does. Thanks to this separation, CBPV can give a crisp account of important concepts in programming languages, including evaluation order (call-by-name vs. call-by-value) and effects (such as memory, exceptions, or probabilities). It is strongly connected to Linear Logic, which gives a different yet related perspective on the same issues.", img: "https://cdn-icons-png.flaticon.com/512/1119/1119022.png" }, { text: "<b>Social choice theory</b> is a theoretical framework for analysis of combining individual opinions, preferences, interests, or welfares to reach a collective decision. Social choice theory dates from Condorcet's formulation of the voting paradox. Social choice blends elements of welfare economics and voting theory. It is methodologically individualistic, in that it aggregates preferences and behaviors of individual members of society. Using elements of formal logic for generality, analysis proceeds from a set of seemingly reasonable axioms of social choice to form a social welfare function.", img: "https://cdn-icons-png.flaticon.com/512/17/17414.png" }, { text: "<b>Distributed systems</b> are groups of networked computers, interacting with each other in order to achieve the same goal. In parallel computing, all processors have access to a shared memory to exchange information between processors. In distributed computing, information is exchanged by passing messages between the processors. Cluster of computers and peer-to-peer systems are examples of such architectures. Models of distributed systems are also used in other science, such as in biology, in order to analyze collective behaviors of autonomous entities interacting with each other by message passing.", img: "https://d1nhio0ox7pgb.cloudfront.net/_img/o_collection_png/dark_grey/256x256/plain/graph.png" }, { text: "<b>Sequent:</b> A sequent represents a theorem by a sequence of hypotheses and the sequence of possible theses they imply. This formalism underlines a symmetry hypotheses/theses ruled by negation and is used in sequent calculus to formalize proofs and to study their properties. Here it is an example of sequent: A , B∨C ⊢ A∧B , A∧C", img: "https://cdn-icons-png.flaticon.com/512/43/43326.png" }, { text: "(Hastad's) <b>switching lemma</b> is a key tool for proving lower bounds on the size of constant-depth Boolean circuits computing some specific Boolean functions. The switching lemma says that depth-2 circuits, in which some fraction of the variables have been set randomly, depend with high probability only on very few variables. Using the switching lemma, Johan Håstad (1987) gave a tight lower bound on the size of constant-depth Boolean circuits computing the parity function using only AND, OR, and NOT logic gates.", img: "https://www.shareicon.net/data/128x128/2015/10/28/663248_switch_512x512.png", }, { text: "<b>Extremal combinatorics</b> studies how large or how small a collection of finite objects can be, if it has to satisfy certain restrictions. For instance, in an n-element set, what is the largest number of subsets of which none contains any other? The question is answered by Sperner's theorem, which gave rise to much of extremal set theory. Another kind of example: How many people can we invite to a party where among each three people there are two who know each other and two who don't know each other? Ramsey theory shows that at most five persons can attend such a party.", img: "https://cdn-icons-png.flaticon.com/512/149/149181.png", }, { text: "<b>Linear programming</b> is a technique for the optimization of a linear function, subject to linear equality and linear inequality constraints. A linear programming algorithm finds a point in the polyhedron of feasible solutions satisfying those constrains, where this function has the smallest (or largest) value. Linear programming is widely used in industries, including transportation, energy, telecommunications, and manufacturing, for diverse types of tasks such as planning, routing, scheduling, assignment, and design.", img: "https://cdn-icons-png.flaticon.com/512/274/274369.png", }, { text: "<b>Bayesian search</b> theory is the application of Bayesian statistics to the search for lost objects. In this setting, a treasure is placed at one location according to a known distribution, and one or more agents are searching for it, aiming to minimize the expected time until the treasure is found. The application of Bayes’ rule is then used to update the prior as new information is obtained during the search.", img: "https://www.shareicon.net/data/128x128/2017/05/22/886152_search_512x512.png", }, { text: "<b>Memory consistency models</b> characterize the effect of concurrent invocations to a library implementing a shared state, e.g., a queue or a key-value map. Strong consistency means that the results of concurrently-executed invocations match the results of some serial execution of those same invocations. Since strong consistency carries a significant penalty on performance, modern implementations provide weaker guarantees known as weak consistency models, e.g., eventual or causal consistency.", img: "https://cdn-icons-png.flaticon.com/512/2165/2165122.png", }, { text: "<b>Random-access memory (RAM)</b> is a form of computer memory that can be read and changed in any order. In contrast, with other direct-access data storage media such as hard disks, CD-RWs, DVD-RWs and the older magnetic tapes and drum memory, RAM allows data items to be read or written in almost the same amount of time irrespective of its physical location.", img: "https://cdn-icons-png.flaticon.com/512/2165/2165122.png", }, { text: "A <b>random-access machine (RAM)</b> is an abstract computational-machine model identical to a multiple-register counter machine with the addition of indirect addressing. At the discretion of an instruction from its finite state machine's TABLE, the machine derives a target register's address either directly from the instruction itself, or indirectly from the contents (e.g. number, label) of the pointer register specified in the instruction.", img: "https://cdn-icons-png.flaticon.com/512/86/86101.png", }, { text: "A <b>labeling algorithm</b> consists in updating a label for each node of a graph until a global optimum is reached. For example, label propagation propagates labels in a graph in order to heuristically detect community structures. As another example, the output of a connected component algorithm often resides in a labeling where two nodes are in the same component iff they have same label. Connected-component labeling is used in computer vision to detect connected regions.", img: "https://static.thenounproject.com/png/366780-200.png", }, { text: "In graph theory, the <b>planarity testing</b> problem is the algorithmic problem of testing whether a given graph can be drawn in the plane without edge intersections. This is a well-studied problem in computer science for which many practical algorithms have emerged. The classic path addition method of Hopcroft and Tarjan was the first published linear-time planarity testing algorithm in 1974.", img: "https://static.thenounproject.com/png/1205037-200.png", }, { text: "In software engineering and hardware engineering, <b>formal methods</b> are a particular kind of mathematically based technique for the specification, development and verification of software and hardware systems. Formal methods use mathematical proofs in order to establish rigorously the reliability of a design. As systems become more complicated, and safety becomes a more important issue, the formal approach to system design offers an additional level of insurance to system testing.", img: "https://static.thenounproject.com/png/718608-200.png", }, { text: "The <b>probabilistic method</b> was pioneered by Paul Erdős for proving the existence of a prescribed kind of mathematical object without exhibiting it explicitly. It consists in proving that if one randomly chooses objects from a specified set, the probability that the result is of the prescribed kind is strictly greater than zero. Although the proof uses probability, the final conclusion is determinist. This method has been applied primarily to combinatorics, and later on to various areas of mathematics and of computer science.", img: "https://cdn-icons-png.flaticon.com/512/445/445130.png", }, { text: "A <b>hybrid system</b> (or hybrid dynamical system) is a dynamical system that exhibits both continuous and discrete dynamic behavior – a system that can both flow (described by a differential equation) and jump (described by a state machine or automaton). Hybrid systems have been used to model several cyber-physical systems, including physical systems with impact, logic-dynamic controllers, and even Internet congestion.", img: "https://cdn-icons-png.flaticon.com/512/40/40404.png", }, { text: "A <b>cyber-physical system</b> is a mechanism that is controlled or monitored by computer-based algorithms. In cyber-physical systems, physical and software components are deeply intertwined, each operating on different spatial and temporal scales. Examples of cyber-physical systems include smart grid, autonomous automobile systems, medical monitoring, process control systems, robotics systems, and automatic pilot avionics.", img: "https://cdn-icons-png.flaticon.com/512/40/40389.png", }, { text: "A discrete-time <b>dynamical system</b> is a map acting on a (usually compact) space. One is generally interested in the study the iterations of the map, and the trajectories and distribution of points it induces. Dynamical systems have widely proved their usefulness for the modeling of physical systems, but they also model numerous phenomena from the digital world: dynamical systems can model the execution of an algorithm, as well as loops in a program. Their study is also in deep connection with information theory.", img: "https://img.icons8.com/metro/52/000000/rotate-left.png", }, { text: "<b>Combinatorics on words</b> studies the combinatorial properties of words and formal languages. Their systematic study has a wide field of applications ranging from number theory to bio-informatics or dynamical systems. Word combinatorics focuses on the study of powers, repetitions and periods. The field also includes the study of extended forms of words such as infinite words, bidimensional infinite words or tilings.", img: "https://img.icons8.com/metro/52/000000/accounting.png", }, { text: "<b>Communication complexity:</b> In theoretical computer science, communication complexity studies the amount of communication required to solve a problem when the input to the problem is distributed among two or more parties. It was introduced by Andrew Yao in 1979, who investigated this notion involving two separated parties, traditionally called Alice and Bob. Lower bounds in communication complexity can be used to prove lower bounds in decision tree complexity, VLSI circuits, data structures, streaming algorithms, space–time tradeoffs for Turing machines and more.", img: "https://cdn-icons-png.flaticon.com/512/46/46878.png", }, { text: "A <b>polyomino</b> is a plane geometric figure formed by joining one or more equal squares edge to edge (such as pieces in Tetris). In statistical physics, the study of polyominoes and their higher-dimensional analogs (which are often referred to as lattice animals) is applied to problems in physics and chemistry. Challenges are often posed for tiling a prescribed region, or the entire plane, with polyominoes, and related problems are investigated in mathematics and computer science.", img: "https://www.irif.fr/_media/actualites/tetris.png", }, { text: "<b>Graph Minor.</b> A graph H is a minor of a graph G if H can be obtained from a subgraph of G by contracting edges. A classical theorem of Kuratowski characterizes planar graphs by the exclusion of two specific minors: the complete graph with 5 nodes and the complete bipartite graph with 3+3 nodes. In a series of papers (700 pages), Robertson and Seymour generalized this result by proving that any family of graphs closed under minor operation can be characterized by finitely many forbidden minors. The ingredients (such as treewidth) of the proof of this theoretical result have rich algorithmic consequences, such as the tractability of detecting a fixed minor, or finding disjoint paths linking prescribed terminals, to give only two examples.", img: "https://cdn.onlinewebfonts.com/svg/img_537569.png", }, { text: "<b>Proof theory</b> is the branch of mathematical logic that studies proofs as mathematical objects. In particular, proof are syntactic constructions built from axioms and inference rules. Relevant to computer science are the studies of computational and complexity aspects of proofs.", img: "https://cdn.onlinewebfonts.com/svg/img_115064.png", }, { text: "The <b>Curry-Howard correspondence</b> defines a direct relationship between well-typed functional programs and mathematical proofs. For instance, a functional program with input of type <i>A</i> and output of type <i>B</i> (i.e., a program of type <i>A</i> → <i>B</i>) is equivalent to a proof of the formula <i>A implies B</i> (i.e., <i>A</i> ⇒ <i>B</i>): it is an operational way to produce a proof of <i>B</i> from a proof of <i>A</i>. This correspondence can be generalized to logics that are more expressive than the implicative fragment of the propositional logic and, nowadays, it has become a standard methodological tool to analyze a logic with respect to its computational aspects and of a calculus with respect to its logical aspects.", img: "https://www.irif.fr/_media/actualites/currry-howard.png", }, { text: "<b>Proof assistant:</b> A proof assistant is a software tool to mechanize reasoning. Such a tool typically ensures the well-foundedness of formal definitions, helps in decomposing a formal proof into intermediate proof goals (i.e., lemmas), and checks that the reasoning steps are logically consistent.", img: "https://static.thenounproject.com/png/165467-200.png", }, { text: "A <b>locality-sensitive hashing</b> is a particular kind of hash function in which, contrary to cryptographic hash functions, there is a positive correlation between the similarity of two elements and the probability of being hashed into the same value. This can be a helpful dimensionality-reduction technique, where the tradeoff between accuracy and speed is skewed towards speed. For instance, they can be used to detect that two images are identical if one is the scaled or rotated version of the other.", img: "https://cdn3.iconfinder.com/data/icons/glypho-travel/64/map-pin-marker-circle-512.png", }, { text: "An <b>emergent algorithm</b> defines rules of behavior for individual simple agents, so as to obtain desirable complex behavior of the set of all agents treated as a whole. For example, a team of collaborating nano-robots may be capable of navigating around obstacles in terrain, even though the program run by the individual nano-robots is unable even to \"understand\" the concept of an obstacle. Examples of emergent algorithms and models include cellular automata, neural networks, and swarm intelligence systems (ant colony optimization, bee colony algorithms, etc.).", img: "https://static.thenounproject.com/png/33274-200.png", }, { text: "<b>Knot theory</b> studies mathematical knots. These are like the usual shoelaces and rope knots but with the difference that the ends of the string are joined together so that it cannot be undone. Of particular interest is the study of when two knots are equivalent, that is when one can be transformed into the other without cutting the string or passing the string through itself. The theory has applications in physics, biology, chemistry, and computer science. For instance, the security of some quantum money relies on the assumption that given two different looking but equivalent knots, it is difficult to explicitly find a transformation that takes one to the other.", img: "https://d30y9cdsu7xlg0.cloudfront.net/png/85813-200.png", }, { text: "<b>Approximation algorithms</b> are algorithms that produce a solution that approximates the best possible solution of an optimization problem. While finding the optimal solution of practical problems is often infeasible, an approximation algorithm usually produces its solution in an efficient way and provides formal guarantees about the quality of the approximation. An example of such a problem is the so-called <i>traveling salesman problem</i> which consists in finding among all possible itineraries the shortest route that allows a salesman to visit a given set of cities and come back home.", img: "https://cdn-icons-png.flaticon.com/512/1774/1774084.png", }, { text: "<b>Biological algorithm:</b> biological algorithm is a term used to describe the biological processes from an algorithmic, or computer scientific, perspective. It concerns questions such as what are the algorithmic challenges faced by the biological organism, and what are the algorithmic principals used in order to overcome these challenges. For example, when a group of ants finds a large piece of food and needs to decide its navigation route back to the nest, what are the benefits and pitfalls of noise in their communication?", img: "https://cdn-icons-png.flaticon.com/512/534/534961.png", }, { text: "<b>Games</b> are mathematical objects used for modeling situations in which several participants/players interact, and each of them aims at fulfilling a personal goal. Real games such as chess or go are cases in which there are two players which are opponent. Games occur in computer science for modeling the logical duality between conjunction and disjunctions, or for defining particular families of complexity classes. Games appear in verification for describing how a system has to react to the environment (the opponent) in order to perform what it has been designed for.", img: "https://www.svgrepo.com/show/143264/tic-tac-toe-game.svg", }, { text: "<b>Algorithm:</b> an algorithm is the formal description of a procedure that is used to solve a class of problems. The description consists in a sequence (of finite length) of operations that are interpreted unambiguously by who/what is executing the algorithm. Every algorithm can be directly executed or simulated by any Turing-complete system.", img: "https://d30y9cdsu7xlg0.cloudfront.net/png/1119891-200.png", }, { text: "A <b>Turing machine</b> is a mathematical model of computation that defines an abstract machine that manipulates symbols on a strip of tape according to a table of rules. Despite the model's simplicity, a Turing machine is a general example of a central processing unit (CPU) that controls all data manipulation done by a computer, with the canonical machine using sequential memory to store data. The Turing machine was invented in 1936 by Alan Turing.", img: "https://cdn-icons-png.flaticon.com/512/3067/3067260.png", }, { text: "<b>Quantum Information</b> is the information stored in a quantum system. A quantum system is composed of one or many qubits: the fundamental unit of quantum information. A qubit is a 2-dimensional vector. The basis encodes two classical values of a bit. Quantum information, i.e. Von Neuman entropy, is the analogous of Shannon entropy for classical information, and it is often used to measure physical properties of a quantum system, like the entanglement.", img: "https://cdn3.iconfinder.com/data/icons/block/32/genius-512.png", }, { text: "<b>Gradual typing</b> is a technique that allows the programmer to control which parts of a program check their type correctness (i.e., that apples are added to apples) before execution and which parts check it during their execution instead. It is often used to <i>gradually</i> add the before-execution check to dynamic languages, like JavaScript, which perform the check only at run-time, since it is generally better to find errors before the execution of a program rather than during its execution.", img: "https://cdn-icons-png.flaticon.com/512/1197/1197460.png", }, { text: "An <b>automaton</b> is a construct made of states designed to determine if a sequence of inputs should be accepted or rejected. It starts from an <i>initial state</i> and when it receives a new input it moves to another state according to the way it was programmed. If at the end of all inputs the automaton is in a state designated as <i>final</i>, then the sequence of inputs is accepted, otherwise it is rejected.", img: "https://www.shareicon.net/data/128x128/2016/04/06/745555_robot_512x512.png", }, { text: "<b>Information dissemination</b> is the process by which a piece of information is propagated in a distributed system through direct communications from node to node. Rumor spreading between humans or broadcasting in a network are two typical examples. Information propagation is a basic building block of many distributed algorithms and its analysis is often critical in understanding their complexity.", img: "https://d1nhio0ox7pgb.cloudfront.net/_img/o_collection_png/dark_grey/256x256/plain/graph.png", }, { text: "<b>Unproductive:</b> A part of a program is unproductive if it performs an infinite number of computing steps without any interaction with the rest of the program or external devices. Unproductive code is basically useless, and may even be unsafe, and detecting parts of code that are unproductive is important to improve software quality.", img: "https://d30y9cdsu7xlg0.cloudfront.net/png/59945-200.png", }, { text: "<b>Polymorphism:</b> A function is polymorphic when it can be applied to arguments of different types. For instance, the identity function <i>fun x = x</i> is polymorphic since it can be applied, say, to integers and Boolean arguments, while the successor function <i>fun x = x+1</i> is not, since it can be applied only to integers.", img: "https://vignette.wikia.nocookie.net/nationstates/images/3/37/Symbol_lambda.png", }, { text: "<b>Machine learning </b> is a research discipline that studies algorithms that can learn a pattern or a model from a set of examples. Most of the algorithms can be framed in the language of statistics or probability theory, but are often mapped to simple linear algebraic operations. Machine learning can be further divided into supervised and unsupervised methods. In supervised machine learning, the training set is composed of vectors along with a label, and the task is to learn the correct label for unseen vectors. In unsupervised learning, the training set is composed of just vectors, and the task is to find implicit relations between the elements of the dataset, a task that often goes under the name of clustering.", img: "https://png.icons8.com/metro/50/000000/for-experienced.png", }, { text: "<b>Full Abstraction:</b> The quest for a fully abstract model for the contextual equivalence of PCF, a paradigmatic functional language, has been influential in the area of programming languages semantics. A model is fully abstract if it is both <i>sound</i> and <i>complete</i>. A denotational model is complete for a given notion of equivalence between programs if equivalent programs have the same denotation, some mathematical object they are mapped to; it is sound if programs having the same denotation are equivalent.", img: "https://cdn-icons-png.flaticon.com/512/603/603737.png", }, { text: "<b>Category:</b> A category is a general algebraic structure that consists in a collection of <i>objects</i> (sets, groups, topological spaces etc.) and, for any two objects A and B, a set of <i>arrows</i> from A to B (maps, group homomorphisms, continuous mappings etc.) equipped with a notion of composition. Categories are a useful abstraction for describing various mathematical structures and even models for logical deductions, most notably intuitionistic logic and the simply-typed lambda-calculus.", img: "https://www.irif.fr/_media/actualites/category.png", }, { text: "<b>Separation logic</b> is a language for describing properties and reasoning about programs that use mutable data structures (i.e. memory cells and pointers). Separation logic has a special support for local reasoning, which is the ability to use and compose properties that involve a subset of the data configuration only: it <i>separates</i> the relevant portion of the data structure from the irrelevant one. Local reasoning gives more compact proofs and specifications for imperative programs than with prior formalisms. Furthermore, it helps with the scalability of proofs done in automatic and semi-automatic verification and program analysis tools.", img: "https://d30y9cdsu7xlg0.cloudfront.net/png/28809-200.png", }, { text: "<b>Clustering: </b> In unsupervised machine learning, clustering is used to partition a set of unlabeled points in clusters of points that share some form of similarity. When clustering, we assume data can be represented in a vector space where distances are a proxy for similarity, such as similar objects are closer than different objects.", img: "https://cdn4.iconfinder.com/data/icons/network-and-sharing-line-icons-vol-1/48/02-512.png", }, { text: "A <b>blockchain</b> is a data structure used to grow a list of records in a collaborative manner. Records are grouped into chained blocks using cryptographic hashing and proof of work in order to make the system robust to attempts of falsification, even when carried out by significant groups of hostile agents. The concept was introduced with Bitcoin cryptocurrency where records are cryptographically signed transactions.", img: "https://static.thenounproject.com/png/1138186-200.png", }, ]; { var day=new Date().getDay(); var index=0; if (day!=-5) { var oneDayInMs = 1000*60*60*24; var currentTimeInMs = new Date().getTime(); // UTC time var timeInDays = Math.floor(currentTimeInMs / oneDayInMs); seed = timeInDays; index = seededRandom(quotes.length); } var quote = quotes[index]; } document.getElementById("quote").innerHTML = '<img ALIGN="left" height="42" width="42" hspace="8" vspace="2" src="' + quote.img + '"/></td><td>' + quote.text ; </script> </p> </div> <h2 class="sectionedit23 page-header pb-3 mb-4 mt-5" id="reseaux_sociaux">Réseaux Sociaux</h2> <p> Suivez nous sur Mastodon, Twitter/X et LinkedIn : </p> <p> <a href="https://www.linkedin.com/company/33222530/admin/feed/posts/" class="media" title="https://www.linkedin.com/company/33222530/admin/feed/posts/" rel="ugc nofollow"><img src="https://www.irif.fr/_media/index.png?w=50&h=50&tok=337bd5" class="media img-responsive" loading="lazy" title="LinkedIn" alt="LinkedIn" width="50" height="50" /></a> <a href="https://twitter.com/IRIF_Paris" class="media" title="https://twitter.com/IRIF_Paris" rel="ugc nofollow"><img src="https://www.irif.fr/_media/twitter-x-logo-graphic-design-itsnicethat-01.width-1440_wgww7xq65qfzl1dm.jpg?w=50&h=50&tok=7457f1" class="media img-responsive" loading="lazy" title="Twitter/X" alt="Twitter/X" width="50" height="50" /></a> <a href="https://mastodon.social/@IRIF" class="media" title="https://mastodon.social/@IRIF" rel="ugc nofollow"><img src="https://www.irif.fr/_media/mastodon_logo.png?w=50&h=50&tok=cb35e6" class="medialeft img-responsive" loading="lazy" title="Mastodon" alt="Mastodon" width="50" height="50" /></a> </p> </div><div class="wrap_column wrap_third plugin_wrap"> <h2 class="sectionedit26 page-header pb-3 mb-4 mt-5" id="actualites">Actualités</h2> <div class="plugin_include_content plugin_include__actualites:index" id="plugin_include__actualites__index"> <div class="plugin_wrap"><span class="bs-wrap bs-wrap-image" data-img-shape="thumbnail"><a href="https://www.irif.fr/_detail/actualites/ressources/gt_lvp_gdr_gpl_logo.png?id=index" class="media" title="actualites:ressources:gt_lvp_gdr_gpl_logo.png"><img src="https://www.irif.fr/_media/actualites/ressources/gt_lvp_gdr_gpl_logo.png?w=60&tok=d0eae5" class="medialeft img-responsive" loading="lazy" alt="" width="60" /></a></span> <p> <em>12.11.2024</em><br/> La <strong>journée du Groupe de Travail LVP</strong> (Langages et à la Vérification de Programme) du GdR <abbr title="GNU General Public License">GPL</abbr> du CNRS se déroulera le <strong>jeudi 14 novembre</strong> 2024<strong> à l'IRIF</strong>, de <strong>9h à 17h40</strong>. <a href="https://www.irif.fr/~gallego/" class="urlextern" title="https://www.irif.fr/~gallego/" rel="ugc nofollow">Emilio Jesús Gallego Aria</a>, chercheur Inria à l'IRIF, Université de Paris donnera d'ailleurs un exposé sur : “Flèche: Incremental Validation for Hybrid Formal Documents”. Cet évènement est gratuit mais l'inscription est obligatoire. <a href="https://groupes.renater.fr/wiki/lvp/public/journee_lvp_novembre2024" rel="nofollow"><i class="dw-icons fa fa-arrow-circle-right" style="" title=""></i></a> </p> <div class="wrap_clear plugin_wrap"></div></div><div class="plugin_wrap"><span class="bs-wrap bs-wrap-image" data-img-shape="thumbnail"><a href="https://www.irif.fr/_detail/actualites/ressources/2025_irif_erc_synergie_grants_winners.png?id=index" class="media" title="actualites:ressources:2025_irif_erc_synergie_grants_winners.png"><img src="https://www.irif.fr/_media/actualites/ressources/2025_irif_erc_synergie_grants_winners.png?w=60&tok=dc435e" class="medialeft img-responsive" loading="lazy" alt="" width="60" /></a></span> <p> <em>5.11.2024</em><br/> Cette année, <strong>trois chercheurs</strong> de l'IRIF font partie de <strong>deux projets</strong> ayant été retenus pour une <strong>bourse Synergie 2025 du Conseil Européen de la Recherche (ERC)</strong>. Toutes nos félicitations à <a href="https://www.irif.fr/~berthe/" class="urlextern" title="https://www.irif.fr/~berthe/" rel="ugc nofollow">Valérie Berthé</a>, <a href="https://pauillac.inria.fr/~herbelin/" class="urlextern" title="https://pauillac.inria.fr/~herbelin/" rel="ugc nofollow">Hugo Herbelin</a> et <a href="https://www.irif.fr/~mellies/" class="urlextern" title="https://www.irif.fr/~mellies/" rel="ugc nofollow">Paul-André Melliès</a> ! Nous leur souhaitons d'obtenir des résultats concluants. </p> <div class="wrap_clear plugin_wrap"></div></div><div class="plugin_wrap"><span class="bs-wrap bs-wrap-image" data-img-shape="thumbnail"><a href="https://www.irif.fr/_detail/actualites/ressources/pp_dexterkozen.jpg?id=index" class="media" title="actualites:ressources:pp_dexterkozen.jpg"><img src="https://www.irif.fr/_media/actualites/ressources/pp_dexterkozen.jpg?w=60&tok=473308" class="medialeft img-responsive" loading="lazy" title="pp_dexterkozen.jpg" alt="pp_dexterkozen.jpg" width="60" /></a></span> <p> <em>31.10.2024</em><br/> L’IRIF est ravi d’accueillir <a href="https://www.cs.cornell.edu/~kozen/" class="urlextern" title="https://www.cs.cornell.edu/~kozen/" rel="ugc nofollow">Dexter Kozen</a> de l’Université Cornell en tant qu'intervenant de nos Distinguished Talks. La conférence aura lieu le <strong>3 décembre 2024 à partir de 11h.</strong> Plus de détails à venir ! <a href="https://www.irif.fr/seminaires/irif/index" rel="nofollow"><i class="dw-icons fa fa-arrow-circle-right" style="" title=""></i></a> </p> <div class="wrap_clear plugin_wrap"></div></div><div class="plugin_wrap"><span class="bs-wrap bs-wrap-image" data-img-shape="thumbnail"><a href="https://www.irif.fr/_detail/actualites/ressources/conf_upc_2.png?id=index" class="media" title="actualites:ressources:conf_upc_2.png"><img src="https://www.irif.fr/_media/actualites/ressources/conf_upc_2.png?w=60&tok=d64c7c" class="medialeft img-responsive" loading="lazy" alt="" width="60" /></a></span> <p> <em>24.10.2024</em><br/> <em><strong>L'informatique a-t-elle un avenir ?</strong></em> Telle est la question qui sera débattue lors de la troisième conférence “On éteint, on réfléchit, on discute”, organisée à l'Université Paris Cité par <a href="https://www.irif.fr/~francoisl/" class="urlextern" title="https://www.irif.fr/~francoisl/" rel="ugc nofollow">François Laroussinie</a>. <a href="https://liedlab.net/annuaire/membre/jose-halloy/" class="urlextern" title="https://liedlab.net/annuaire/membre/jose-halloy/" rel="ugc nofollow">José Halloy</a> (LIED) et <a href="https://www.lisn.upsaclay.fr/membres/ligozat-anne-laure/" class="urlextern" title="https://www.lisn.upsaclay.fr/membres/ligozat-anne-laure/" rel="ugc nofollow">Anne-Laure Ligozat</a> (LISN) sont les conférenciers invités. Elle se tiendra le mardi <strong>10 décembre 2024</strong>, de <strong>16h15 à 18h30</strong>. Cet événement est gratuit. <a href="https://www.informatique.univ-paris-diderot.fr/ufr/conferences_ufr" rel="nofollow"><i class="dw-icons fa fa-arrow-circle-right" style="" title=""></i></a> </p> <div class="wrap_clear plugin_wrap"></div></div><div class="plugin_wrap"><span class="bs-wrap bs-wrap-image" data-img-shape="thumbnail"><a href="https://www.irif.fr/_detail/actualites/ressources/perso-sergio-rajsbaum.jpg?id=index" class="media" title="actualites:ressources:perso-sergio-rajsbaum.jpg"><img src="https://www.irif.fr/_media/actualites/ressources/perso-sergio-rajsbaum.jpg?w=60&tok=3c5450" class="medialeft img-responsive" loading="lazy" title="perso-sergio-rajsbaum.jpg" alt="perso-sergio-rajsbaum.jpg" width="60" /></a></span> <p> <em>24.10.2024</em><br/> Le prix de l'Innovation a été décerné à <a href="https://www.irif.fr/users/rajsbaum/index" class="urlextern" title="https://www.irif.fr/users/rajsbaum/index" rel="ugc nofollow">Sergio Rajsbaum</a>, membre associé de l'IRIF, dans le cadre de son <strong>importante contribution à l'Informatique Distribuée</strong>. Ce prix lui sera remis lors de la conférence <strong>SIROCCO'25</strong> à Delphes, en Grèce. <a href="https://www.torontomu.ca/sirocco-2025/call-for-papers/" rel="nofollow"><i class="dw-icons fa fa-arrow-circle-right" style="" title=""></i></a> </p> <div class="wrap_clear plugin_wrap"></div></div><div class="plugin_wrap"><span class="bs-wrap bs-wrap-image" data-img-shape="thumbnail"><a href="https://www.irif.fr/_detail/actualites/ressources/jlkrivine_lesdecompilateurs.jpg?id=index" class="media" title="actualites:ressources:jlkrivine_lesdecompilateurs.jpg"><img src="https://www.irif.fr/_media/actualites/ressources/jlkrivine_lesdecompilateurs.jpg?w=60&tok=1bc38b" class="medialeft img-responsive" loading="lazy" title="jlkrivine_lesdecompilateurs.jpg" alt="jlkrivine_lesdecompilateurs.jpg" width="60" /></a></span> <p> <em>30.9.2024</em><br/> <a href="https://www.irif.fr/~krivine/" class="urlextern" title="https://www.irif.fr/~krivine/" rel="ugc nofollow">Jean-Louis Krivine</a>, professeur émérite à l'IRIF, a publié un livre, “Les décompilateurs - L'Univers en tête”. Vous y trouverez, entre autres, une réflexion sur l'<strong>origine des mathématiques</strong> et le <strong>lien entre logique et informatique théorique</strong> ainsi que quelques <strong>paradoxes en mécanique quantique</strong>. <a href="https://www.eyrolles.com/Sciences/Livre/les-decompilateurs-9782493230232/" rel="nofollow"><i class="dw-icons fa fa-arrow-circle-right" style="" title=""></i></a> </p> <div class="wrap_clear plugin_wrap"></div></div><div class="plugin_wrap"><span class="bs-wrap bs-wrap-image" data-img-shape="thumbnail"><a href="https://www.irif.fr/_detail/actualites/ressources/affichefds2024.jpg?id=index" class="media" title="actualites:ressources:affichefds2024.jpg"><img src="https://www.irif.fr/_media/actualites/ressources/affichefds2024.jpg?w=60&tok=9c7c97" class="medialeft img-responsive" loading="lazy" title="affichefds2024.jpg" alt="affichefds2024.jpg" width="60" /></a></span> <p> <em>4.10.2024</em><br/> La <strong>Fête de la Science édition 2024</strong> est lancée ! L'IRIF et l'Université Paris Cité accueilleront du <strong>4 au 14 octobre</strong>, 13 classes de primaire et collège, qui viendront découvrir l'informatique à travers des <strong>activités débranchées</strong> et de la <strong>programmation</strong>. Nous proposons également un <strong>programme quantique</strong> créé avec le laboratoire <a href="https://mpq.u-paris.fr/" class="urlextern" title="https://mpq.u-paris.fr/" rel="ugc nofollow">Matériaux et Phénomènes Quantiques</a> (MPQ) à des classes de lycée. <a href="https://www.irif.fr/mediation/fdls" rel="nofollow"><i class="dw-icons fa fa-arrow-circle-right" style="" title=""></i></a> </p> <div class="wrap_clear plugin_wrap"></div></div><div class="plugin_wrap"><span class="bs-wrap bs-wrap-image" data-img-shape="thumbnail"><a href="https://www.irif.fr/_detail/actualites/ressources/pp_melissa_godde.jpg?id=index" class="media" title="actualites:ressources:pp_melissa_godde.jpg"><img src="https://www.irif.fr/_media/actualites/ressources/pp_melissa_godde.jpg?w=60&tok=e3eef5" class="medialeft img-responsive" loading="lazy" title="pp_melissa_godde.jpg" alt="pp_melissa_godde.jpg" width="60" /></a></span> <p> <em>18.10.2024</em><br/> Nous souhaitons la bienvenue à <strong>Mélissa Goddé, nouvelle gestionnaire</strong>, qui vient renforcer l'équipe administrative. <a href="https://www.irif.fr/users/godde/index" rel="nofollow"><i class="dw-icons fa fa-arrow-circle-right" style="" title=""></i></a> </p> <div class="wrap_clear plugin_wrap"></div></div><div style='display:none'><div class="wrap_right plugin_wrap"> <p> <span class="bs-wrap bs-wrap-button" data-btn-type="primary" data-btn-size="xs" data-btn-icon="fa fa-pencil-square-o"><a href="https://www.irif.fr/admindb/actus/" class="urlextern" title="https://www.irif.fr/admindb/actus/" rel="ugc nofollow">edit</a></span> </p> </div></div></div> <div class="wrap_right plugin_wrap"> <p> <span class="bs-wrap bs-wrap-button" data-btn-type="primary" data-btn-size="xs" data-btn-icon="fa fa-arrow-circle-right"><a href="https://www.irif.fr/actualites/all" class="wikilink1" title="actualites:all" data-wiki-id="actualites:all">toutes les anciennes actualités</a></span> </p> </div> <p> <br/> (Ces actualités sont présentées selon un classement mêlant priorité et aléatoire.) </p> </div><div class="wrap_column wrap_third plugin_wrap"> <h2 class="sectionedit51 page-header pb-3 mb-4 mt-5" id="agenda">Agenda</h2> <div class="plugin_include_content plugin_include__agenda" id="plugin_include__agenda"> <div class="plugin_include_content plugin_include__seminaires:weekseminars" id="plugin_include__seminaires__weekseminars"> <p> <a href="https://www.irif.fr/seminaires/verif/index" class="wikilink1" title="seminaires:verif:index" data-wiki-id="seminaires:verif:index">Vérification</a><br/> Lundi 25 novembre 2024, 11 heures, Salle 3052<br/> <strong>Laetitia Laversa</strong> (IRIF) <em>Execution-time Opacity Control for Timed Automata</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b11-405"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b11-405"><div class="bs-wrap bs-wrap-well well well-sm"> Timing leaks in timed automata (TA) can occur whenever an attacker is able to deduce a secret by observing some timed behavior. In execution-time opacity, the attacker aims at deducing whether a private location was visited, by observing only the execution time. It can be decided whether a TA is opaque in this setting. In the work presented in this talk, we tackle control, and show that we are able to decide whether a TA can be controlled at runtime to ensure opacity. Our method is constructive, in the sens that we can exhibit such a controller. </div> </div> <p> <a href="https://www.irif.fr/seminaires/programmation/index" class="wikilink1" title="seminaires:programmation:index" data-wiki-id="seminaires:programmation:index">Programmation</a><br/> Lundi 25 novembre 2024, 15 heures 30, 3052<br/> <strong>Alexandre Moine</strong> (NYU) <em>Reaching for Unreachability Properties in Separation Logic</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b14-406"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b14-406"><div class="bs-wrap bs-wrap-well well well-sm"> Unreachability is a property at the heart of garbage collection: if a location is unreachable, it can be safely deallocated. However, formally reasoning about unreachability is challenging. Indeed, to prove that a location is unreachable, one has to consider the whole heap and possibly multiple concurrent stacks, making local reasoning apparently out of reach. In this talk, I will present two projects tackling the challenge of unreachability. <p> In the first part, I will present my PhD thesis work: an Iris-fueled Separation Logic with space credits, allowing for the verification of heap space bounds in the presence of concurrency and garbage collection. Crucially, this logic tracks the reachability of heap objects in a modular way, and allows for recovering space credits when the user proves an object unreachable. </p> <p> In the second part, I will present another line of work about disentanglement. Disentanglement is a property of parallel programs asserting that a location allocated by a task must remain unreachable by concurrently executing tasks. Making use of disentanglement, the MPL (MaPLe) compiler for parallel ML equips programs with a blazingly fast, task-local, garbage collector. I will present DisLog, an Iris-fueled Separation Logic for verifying disentanglement, and present ongoing work on TypeDis, a type system for automatically verifying disentanglement. </div> </p> </div> <p> <a href="https://www.irif.fr/seminaires/picube/index" class="wikilink1" title="seminaires:picube:index" data-wiki-id="seminaires:picube:index">Formath</a><br/> Lundi 25 novembre 2024, 15 heures 30, 3052<br/> <strong>Alexandre Moine</strong> (Courant Institute, New York University) <em>Reaching for Unreachability Properties in Separation Logic</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b32-407"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b32-407"><div class="bs-wrap bs-wrap-well well well-sm"> Unreachability is a property at the heart of garbage collection: if a location is unreachable, it can be safely deallocated. However, formally reasoning about unreachability is challenging. Indeed, to prove that a location is unreachable, one has to consider the whole heap and possibly multiple concurrent stacks, making local reasoning apparently out of reach. In this talk, I will present two projects tackling the challenge of unreachability. <p> In the first part, I will present my PhD thesis work: an Iris-fueled Separation Logic with space credits, allowing for the verification of heap space bounds in the presence of concurrency and garbage collection. Crucially, this logic tracks the reachability of heap objects in a modular way, and allows for recovering space credits when the user proves an object unreachable. </p> <p> In the second part, I will present another line of work about disentanglement. Disentanglement is a property of parallel programs asserting that a location allocated by a task must remain unreachable by concurrently executing tasks. Making use of disentanglement, the MPL (MaPLe) compiler for parallel ML equips programs with a blazingly fast, task-local, garbage collector. I will present DisLog, an Iris-fueled Separation Logic for verifying disentanglement, and present ongoing work on TypeDis, a type system for automatically verifying disentanglement. </div> </p> </div> <p> <a href="https://www.irif.fr/seminaires/combi/index" class="wikilink1" title="seminaires:combi:index" data-wiki-id="seminaires:combi:index">Combinatoire énumérative et analytique</a><br/> Mardi 26 novembre 2024, 11 heures, Salle 3071<br/> <strong>Guillem Perarnau</strong> <em>Extremal stationary values for random digraphs</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b2-408"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b2-408"><div class="bs-wrap bs-wrap-well well well-sm"> In this talk, we will explore the extremal values of the stationary distribution of random walks on sparse directed random graphs with given degrees. While the stationary distribution in undirected graphs is determined by the degrees, in the directed case, the graph's geometry plays a crucial role. In the first part of the talk, we will discuss the minimum positive stationary value and its implications for the hitting and cover times of such random graphs. In the second part, we will focus on the maximum stationary value, which is intimately connected with the maximum in-degree. We will highlight the case where the in-degrees exhibit power-law behavior and relate it to the power-law hypothesis of the PageRank walk. This talk is based on joint work with Xing Shi Cai, Pietro Caputo, and Matteo Quattropani. </div> </div> <p> <a href="https://www.irif.fr/seminaires/numeration/index" class="wikilink1" title="seminaires:numeration:index" data-wiki-id="seminaires:numeration:index">One world numeration seminar</a><br/> Mardi 26 novembre 2024, 14 heures, Online<br/> <strong>Haojie Ren</strong> (Technion) <em>The dimension of Bernoulli convolutions in $\mathbb{R}^d$</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b28-409"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b28-409"><div class="bs-wrap bs-wrap-well well well-sm"> For $(\lambda_{1},\dots,\lambda_{d})=\lambda\in(0,1)^{d}$ with $\lambda_{1}>\cdots>\lambda_{d}$, denote by $\mu_{\lambda}$ the Bernoulli convolution associated to $\lambda$. That is, $\mu_{\lambda}$ is the distribution of the random vector $\sum_{n\ge0}\pm\left(\lambda_{1}^{n},\dots,\lambda_{d}^{n}\right)$, where the $\pm$ signs are chosen independently and with equal weight. Assuming for each $1\le j\le d$ that $\lambda_{j}$ is not a root of a polynomial with coefficients $\pm1,0$, we prove that the dimension of $\mu_{\lambda}$ equals $\min\{ \dim_{L}\mu_{\lambda},d\} $, where $\dim_{L}\mu_{\lambda}$ is the Lyapunov dimension. This is a joint work with Ariel Rapaport. </div> </div> <p> <a href="https://www.irif.fr/seminaires/these/index" class="wikilink1" title="seminaires:these:index" data-wiki-id="seminaires:these:index">Soutenances de thèses</a><br/> Mercredi 27 novembre 2024, 14 heures 30, Salle 3052, Bâtiment Sophie Germain<br/> <strong>Alexandra Rogova</strong> (IRIF) <em>Design principles of property graph languages, a theoretical and experimental study</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b21-410"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b21-410"><div class="bs-wrap bs-wrap-well well well-sm"> In the last 50 years, the amount and complexity of information stored in databases has grown and the needs of database users have evolved. These changes have led to the creation of new models such as XML, key-value stores, time series databases and so on. The subject of this thesis is one such model: the graph database. In a graph database, data is stored as a “graph”, or a collection of nodes, representing the entities, connected together by edges, representing relationships between the entities. Additional information about the entities and their relationships can be attached to the nodes and edges. This powerful model, popularized by Neo4j in 2010, is now a staple in various industries such as biology, social networks and banking. By putting the links between the data points front and center, graph databases allow users to reason not only about individual elements but also about the structure of the graph. Accordingly, the goal of a typical graph query is to find a “path” connecting specific nodes. <br/> <br/> Because graph traversals inherently rely on transitivity, traditional query languages are not suitable in the graph context, and thus new languages have been created. In the theoretical community, the basic building blocks of a graph language are the Regular Path Queries (RPQs), which define path constraints by way of regular expressions. The expressive power and complexity of RPQs and their extensions (by union, conjunction, two-way navigation, data value comparisons and path properties for example) have been studied since the 1990s but their properties are barely beginning to be understood. <br/> <br/> The most popular practical graph language today is Neo4j’s Cypher. In Cypher, a path can be described by a regular expression but it also includes many other features among which aggregation, different path semantics, projection, subqueries and updates. These elements differ from those of other languages, like Tigergraphs’ GSQL, or Oracle’s PGQL, but all graph systems share the same kernel: pattern matching. <br/> <br/> In 2019, a new International Organisation for Standardization (ISO) group was created to oversee the standardization of practical graph languages. This led to two new standards: SQL/PGQ and GQL. The idea of SQL/PGQ is to add a view-based pattern matching mechanism to SQL and interpret the relational data as a graph only when necessary, whereas GQL is standalone and stores the data as a native graph. While this standardization work is a step in the right direction, there is one crucial ingredient missing: a corresponding theoretical model. <br/> <br/> The goal of this thesis is to define a theoretical language for graph databases, akin to relational algebra for SQL, that reflects the essential aspects of GQL and SQL/PGQ while being simple enough for theoretical study. We start by presenting in detail the pattern matching features shared by SQL/PGQ and GQL. We then identify and formalize the core of this language. Afterwards, we position our formalisations of SQL/PGQ and GQL in comparison to relational algebra, which allows us to highlight their distinct styles, while also proving their equivalence. Finally, we explore the impact of extending pattern matching with list functions and show that this addition is not only dangerous in theory, but also fails in practice. </div> </div> <p> <a href="https://www.irif.fr/seminaires/pps/index" class="wikilink1" title="seminaires:pps:index" data-wiki-id="seminaires:pps:index">Preuves, programmes et systèmes</a><br/> Jeudi 28 novembre 2024, 9 heures 30, Amphithéâtre Alan Turing<br/> <strong>Membres De Pps</strong> <em>Journée de rentrée PPS</em> </p> <p> <a href="https://www.irif.fr/seminaires/cat/index" class="wikilink1" title="seminaires:cat:index" data-wiki-id="seminaires:cat:index">Catégories supérieures, polygraphes et homotopie</a><br/> Vendredi 29 novembre 2024, 14 heures, Salle 1013<br/> <strong>Elies Harington</strong> (LIX) <em>Cohomologie en HoTT : une traduction mot à mot du langage faisceautique en théorie des types</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b3-411"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b3-411"><div class="bs-wrap bs-wrap-well well well-sm"> La cohomologie d'un espace est classiquement définie à partir de son complexe de cochaînes singulier. Ce-dernier n'étant pas lui-même un invariant homotopique, on ne peut pas espérer une définition similaire de la cohomologie en HoTT. À la place, on passe par la représentabilité de la cohomologie par les espaces d'Eilenberg-Maclane K(G,n). Le but de cet exposé est de montrer comment traduire mot à mot le langage des torseurs et des gerbes de la théorie des faisceaux vers la théorie des types pour aboutir à la construction de types K(G,1) et K(G,2). </div> </div> <p> <a href="https://www.irif.fr/seminaires/automates/index" class="wikilink1" title="seminaires:automates:index" data-wiki-id="seminaires:automates:index">Automates</a><br/> Vendredi 29 novembre 2024, 14 heures, Salle 3052<br/> <strong>Antonio Casares</strong> (University of Warsaw) <em>Canonical models in automata theory</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b5-412"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b5-412"><div class="bs-wrap bs-wrap-well well well-sm"> Abstract: Automata over finite words are amazing (no need to justify this in the automata seminar). A central reason for their amazingness is the existence of canonical models, which allows for efficient minimization and learning algorithms, as well as for plenty of other theoretical applications. Automata have been extended to operate over richer classes of structures (such as infinite words, trees and graphs), and to define functions using various forms of transducers. However, the theory of these more general automata is often limited, due to the absence of canonical models. In this talk, I will present the subject of my CNRS project: Identifying canonical models for automata over richer classes of structures, with a special focus on automata over infinite words. </div> </div> <p> <a href="https://www.irif.fr/seminaires/verif/index" class="wikilink1" title="seminaires:verif:index" data-wiki-id="seminaires:verif:index">Vérification</a><br/> Vendredi 29 novembre 2024, 11 heures, Salle 3052<br/> <strong>Raya Elsaleh</strong> (Hebrew University of Jerusalem) <em>The Road to Improving Neural Network Verifiers</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b11-413"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b11-413"><div class="bs-wrap bs-wrap-well well well-sm"> Deep neural networks are becoming key components in diverse systems, but these systems often function as “black boxes,” making it difficult to verify their correctness. This opacity is particularly concerning for safety-critical applications like autonomous vehicles, where reliability is essential. Recent advances in neural network verification aim to address these challenges by formally analyzing network behavior. However, verification remains challenging, particularly due to scalability issues and the complexity of DNN verifiers, which can themselves be prone to errors. In this talk, I will review recent developments in neural network verification approaches. Additionally, I will introduce a delta-debugging technique designed to minimize inputs that trigger bugs in the verifiers by reducing network size, thereby streamlining the debugging process for more reliable outcomes. </div> </div></div> </div> </div></div> </div></div><p> <style> .page a.urlextern, .page a.interwiki, .page a.windows, .page a.mail, .page a.media { padding-left: 0 !important; background: none !important; } .page { text-align: justify; } body {font-size: 15px; font-weight: 300; color: #333333; } b,strong {font-weight: 600; color: #333333; } p {margin-bottom:1.3em} h1 {font-size: 2.8em; margin-bottom:1.5em; font-weight: 400; } h2 {font-size: 2.2em; margin-bottom:1.2em; font-weight: 400; } h3 {font-size: 1.9em; margin-bottom:0.9em; font-weight: 400; } h4 {font-size: 1.7em; margin-bottom:0.8em; font-weight: 300; } h5 {font-size: 1.5em; margin-bottom:0.8em; font-weight: 300; } h5 {font-size: 1.4em; margin-bottom:0.8em; font-weight: 300; } </style> </p> </div> </div> <div class="small text-right"> </div> </article> </div> </main> <footer id="dw__footer" class="dw-container py-5 dokuwiki container-fluid">  <div class="dw-container small container-fluid mx-5"> <div class="footer-dw-title"> <div class="media"> <div class="media-left">  <img src="https://www.irif.fr/_media/logo_footer.png" alt="" class="media-object" style="height:10px" /> </div> <div class="media-body"> <div class="row"> <div class="col-sm-2"> <h4 class="media-heading"></h4> <p> </p> </div> <div class="col-sm-10"> </div> </div> </div> </div> </div> <a style="font-size:12px" href="https://www.irif.fr/informations/mentions-legales">Mentions légales</a> <div class="footer-license row"> <hr/> <div id="dw__license" class="col-sm-6"> </div> <div class="col-sm-6"> </div> </div> </div>  </footer> <a href="#dokuwiki__top" class="back-to-top hidden-print btn btn-default" title="Aller au contenu" accesskey="t"> <span class="iconify" data-icon="mdi:chevron-up"></span> </a> <div id="screen__mode"> <span class="visible-xs-block"></span> <span class="visible-sm-block"></span> <span class="visible-md-block"></span> <span class="visible-lg-block"></span> </div> <img src="https://www.irif.fr/lib/exe/taskrunner.php?id=index&1732394068" width="2" height="1" alt="" /> </div> </body> </html>