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=61a6ee3a3e4185dd1cf55b36d7bda871"/> <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=61a6ee3a3e4185dd1cf55b36d7bda871" 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" >Environnement</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 LinkedIn, Bluesky et Mastodon : </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://bsky.app/profile/irif-paris.bsky.social" class="media" title="https://bsky.app/profile/irif-paris.bsky.social" rel="ugc nofollow"><img src="https://www.irif.fr/_media/logo_blusky.png?w=200&tok=ecec31" class="media img-responsive" loading="lazy" title=" Bluesky" alt=" Bluesky" width="200" /></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="media 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/stoc_2025.jpg?id=index" class="media" title="actualites:ressources:stoc_2025.jpg"><img src="https://www.irif.fr/_media/actualites/ressources/stoc_2025.jpg?w=60&tok=abc66b" class="medialeft img-responsive" loading="lazy" title="stoc_2025.jpg" alt="stoc_2025.jpg" width="60" /></a></span> <p> <em>10.2.2025</em><br/> Félicitations à <a href="https://www.adrianvladu.org/" class="urlextern" title="https://www.adrianvladu.org/" rel="ugc nofollow">Adrian Vladu</a>, membre de l'IRIF, dont l'<strong>article a été accepté à STOC 2025</strong>, une conférence ACM : <a href="https://acm-stoc.org/stoc2025/" 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/cnrs_editions_lecalculadecouvert.jpg?id=index" class="media" title="actualites:ressources:cnrs_editions_lecalculadecouvert.jpg"><img src="https://www.irif.fr/_media/actualites/ressources/cnrs_editions_lecalculadecouvert.jpg?w=60&tok=3c2cfb" class="medialeft img-responsive" loading="lazy" title="cnrs_editions_lecalculadecouvert.jpg" alt="cnrs_editions_lecalculadecouvert.jpg" width="60" /></a></span> <p> <em>10.2.2025</em><br/> <a href="https://www.cnrseditions.fr/" class="urlextern" title="https://www.cnrseditions.fr/" rel="ugc nofollow">CNRS EDITIONS</a> a publié un nouvel ouvrage sur <strong>l'histoire du calcul</strong>, intitulé <strong>𝐿𝑒 𝑐𝑎𝑙𝑐𝑢𝑙 𝑎̀ 𝑑𝑒́𝑐𝑜𝑢𝑣𝑒𝑟𝑡</strong>. Plusieurs chercheurs actuels et anciens de l'IRIF ont contribué à la rédaction de ce livre en rédigeant des chapitres : <br/> ◻️ Partie 4 : ▪️ <em class="u">Chapitre 1</em> - 𝑳'𝒂𝒍𝒈𝒐𝒓𝒊𝒕𝒉𝒎𝒆 : 𝒗𝒆𝒓𝒔 𝒍𝒂 𝒓𝒆́𝒔𝒐𝒍𝒖𝒕𝒊𝒐𝒏 𝒄𝒐𝒏𝒄𝒓𝒆̀𝒕𝒆 𝒅𝒆 𝒑𝒓𝒐𝒃𝒍𝒆̀𝒎𝒆𝒔 - <a href="https://fr.wikipedia.org/wiki/Claire_Mathieu" class="urlextern" title="https://fr.wikipedia.org/wiki/Claire_Mathieu" rel="ugc nofollow">Claire Mathieu</a> <br/> ▪️ <em class="u">Chapitre 2</em> - 𝑳𝒂 𝒄𝒐𝒎𝒑𝒍𝒆𝒙𝒊𝒕𝒆́ 𝒂𝒍𝒈𝒐𝒓𝒊𝒕𝒉𝒎𝒊𝒒𝒖𝒆 - <a href="https://www.irif.fr/users/sperifel/index" class="urlextern" title="https://www.irif.fr/users/sperifel/index" rel="ugc nofollow">Sylvain Perifel</a> <br/> ◻️ Partie 9 : ▪️ <em class="u">Chapitre 1</em> - 𝑳𝒆𝒔 𝒇𝒐𝒏𝒅𝒆𝒎𝒆𝒏𝒕𝒔 𝒅𝒖 𝒄𝒂𝒍𝒄𝒖𝒍 𝒒𝒖𝒂𝒏𝒕𝒊𝒒𝒖𝒆 - <a href="https://www.irif.fr/~magniez/" class="urlextern" title="https://www.irif.fr/~magniez/" rel="ugc nofollow">Frédéric Magniez</a> <a href="https://www.cnrseditions.fr/catalogue/histoire-des-sciences/le-calcul-a-decouvert/" 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/esop.png?id=index" class="media" title="actualites:ressources:esop.png"><img src="https://www.irif.fr/_media/actualites/ressources/esop.png?w=60&tok=59bcb2" class="medialeft img-responsive" loading="lazy" alt="" width="60" /></a></span> <p> <em>30.1.2025</em><br/> <strong>Trois articles</strong> de membres de l'IRIF ont été acceptés à <strong>ESOP 2025</strong>. Félicitations à <a href="https://www.irif.fr/~gio/index.xhtml" class="urlextern" title="https://www.irif.fr/~gio/index.xhtml" rel="ugc nofollow">Giovanni Bernardi</a>, <a href="https://www.irif.fr/~ehrhard/" class="urlextern" title="https://www.irif.fr/~ehrhard/" rel="ugc nofollow">Thomas Ehrhard</a>, <a href="https://www.irif.fr/~faggian/" class="urlextern" title="https://www.irif.fr/~faggian/" rel="ugc nofollow">Claudia Faggian</a> et <a href="https://www.irif.fr/users/manara/index" class="urlextern" title="https://www.irif.fr/users/manara/index" rel="ugc nofollow">Giulia Manara</a> ! <a href="https://etaps.org/2025/programme/" 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/logo-irif.png?id=index" class="media" title="actualites:ressources:logo-irif.png"><img src="https://www.irif.fr/_media/actualites/ressources/logo-irif.png?w=60&tok=e0ab4a" class="medialeft img-responsive" loading="lazy" alt="" width="60" /></a></span> <p> <em>22.1.2025</em><br/> Le <strong>troisième Paris ACTS</strong>, aura lieu à l'IRIF, le <strong>mercredi 29 janvier</strong>. P-ACTS est une série de <strong>séminaires</strong> centrés sur les <strong>connexions entre la théorie des automates et la théorie de la concurence, partagés entre l'EPITA, l'IRIF et le LIX</strong>. Les deux intervenants seront <a href="https://l-laversa.github.io/" class="urlextern" title="https://l-laversa.github.io/" rel="ugc nofollow">Laetitia Laversa</a> et <a href="https://www.cl.cam.ac.uk/~gw104/" class="urlextern" title="https://www.cl.cam.ac.uk/~gw104/" rel="ugc nofollow">Glynn Winskel</a>. Les conférences seront également diffusées sur <strong>Zoom</strong>. Pour les <strong>résumés</strong> et <strong>plus d'informations</strong> sur le séminaire, voir cette page: <a href="https://p-acts.github.io/index.html" 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/fossacs.png?id=index" class="media" title="actualites:ressources:fossacs.png"><img src="https://www.irif.fr/_media/actualites/ressources/fossacs.png?w=60&tok=45da0d" class="medialeft img-responsive" loading="lazy" alt="" width="60" /></a></span> <p> <em>30.1.2025</em><br/> Félicitations à <a href="https://www.irif.fr/users/ebauer/index" class="urlextern" title="https://www.irif.fr/users/ebauer/index" rel="ugc nofollow">Esaïe Bauer</a> et <a href="https://www.irif.fr/users/saurin/index" class="urlextern" title="https://www.irif.fr/users/saurin/index" rel="ugc nofollow">Alexis Saurin</a> dont le <strong>papier à été accepté</strong> pour la conférence <strong>FoSSaCS 2025</strong> ! <a href="https://etaps.org/2025/programme/" 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/logo-irif.png?id=index" class="media" title="actualites:ressources:logo-irif.png"><img src="https://www.irif.fr/_media/actualites/ressources/logo-irif.png?w=60&tok=e0ab4a" class="medialeft img-responsive" loading="lazy" alt="" width="60" /></a></span> <p> <em>7.1.2025</em><br/> Nous sommes heureux d'accueillir notre nouvelle responsable financière et comptable, <a href="https://www.irif.fr/users/dordoigne/index" class="urlextern" title="https://www.irif.fr/users/dordoigne/index" rel="ugc nofollow">Chafia Dordoigne</a>. Vous pouvez la rencontrer dans le bureau 4002. </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/irif_voeux_2025.png?id=index" class="media" title="actualites:ressources:irif_voeux_2025.png"><img src="https://www.irif.fr/_media/actualites/ressources/irif_voeux_2025.png?w=60&tok=9eacf4" class="medialeft img-responsive" loading="lazy" alt="" width="60" /></a></span> <p> <em>6.1.2025</em><br/> L'IRIF vous souhaite une excellente année, riche en découvertes scientifiques, en succès académiques et en épanouissement personnel ! </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="sectionedit49 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 17 février 2025, 11 heures, 3052 and <a href="https://u-paris.zoom.us/j/87460234504?pwd=mVUPogiquRZpL0HxEVffccgKRTZ1ID.1" class="urlextern" title="https://u-paris.zoom.us/j/87460234504?pwd=mVUPogiquRZpL0HxEVffccgKRTZ1ID.1" rel="ugc nofollow">Zoom link</a><br/> <strong>Niklas Kochdumper</strong> (IRIF) <em>Robust Identification of Hybrid Automata from Noisy Data</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b11-279"><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-279"><div class="bs-wrap bs-wrap-well well well-sm"> In recent years, many different methods for identifying hybrid automata from data have been proposed. However, most of these methods consider clean simulator data, and consequently do not perform well for noisy data measured from real systems. We address this shortcoming with a new approach for the identification of hybrid automata that is specifically designed to be robust to noise. In particular, we propose a new high-level strategy consisting of the following three steps: clustering based on the dynamics identified from a local dataset, state space partitioning using decision trees, and conversion of the decision tree to a hybrid automaton. In addition, we introduce several new concepts for the realization of the single steps. For example, we propose an automated regularization of the dynamic models used for clustering via rank adaption, as well as a new variant of the Gini impurity index for decision tree learning, tailored toward hybrid systems where different dynamics can be active within the same state space region. As our experiments on 19 challenging benchmarks with different characteristics demonstrate, in addition to being robust to both process and measurement noise, our approach avoids the need for extensive hyper-parameter tuning and also performs well for clean data without noise. </div> </div> <p> <a href="https://www.irif.fr/seminaires/adg/index" class="wikilink1" title="seminaires:adg:index" data-wiki-id="seminaires:adg:index">Algorithmique distribuée et graphes</a><br/> Mardi 18 février 2025, 15 heures, 3052<br/> <strong>Bernadette Charron-Bost</strong> (Ens Paris) <em>Know your audience (Communication models and function computability in anonymous networks)</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b10-280"><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="b10-280"><div class="bs-wrap bs-wrap-well well well-sm"> In this talk, we present exact characterizations of the functions that are computable in anonymous networks with varying assumptions in the degree of awareness or control that agents have over their outneighbors. First, we characterize the computable functions in the “blind broadcast” model, i.e., when agents have no information on their outgoing neighborhoods. Then we enrich this communication model with either output port awareness, bidirectional channels, or outdegree awareness: In each case, we prove that a function can be computed if and only it is frequency-based, namely, its value only depends on the frequencies of the different input values. This characterization holds for both exact and approximate computability. If one or several nodes are distinguished as leaders, or if the cardinality of the network is known, then under any of the above three assumptions it becomes possible to compute any symmetric function. </div> </div> <p> <a href="https://www.irif.fr/seminaires/semantique/index" class="wikilink1" title="seminaires:semantique:index" data-wiki-id="seminaires:semantique:index">Sémantique</a><br/> Mardi 18 février 2025, 15 heures, Salle 3071<br/> <strong>Quentin Aristote</strong> <em>Monotone weak distributive laws over the lifted powerset monad in categories of algebras</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b15-281"><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="b15-281"><div class="bs-wrap bs-wrap-well well well-sm"> Noticing the similarity between the monotone weak distributive laws combining two layers of non-determinism in sets and in compact Hausdorff spaces, we study whether the latter law can be obtained automatically as a weak lifting of the former. This holds partially, but does not generalize to other categories of algebras: we then characterize when exactly monotone weak distributive laws over powerset monads in categories of algebras exist, exhibiting a law combining probabilities and non-determinism in compact Hausdorff spaces and showing on the other hand that such laws do not exist in a lot of other cases. </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 18 février 2025, 14 heures, Online<br/> <strong>Neil Macvicar</strong> (Queen's University) <em>Intersecting Cantor sets generated by Complex Radix Expansions</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b28-282"><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-282"><div class="bs-wrap bs-wrap-well well well-sm"> Consider the classical middle third Cantor set. This is a self-similar set containing all the numbers in the unit interval which have a ternary expansion that avoids the digit 1. We can ask when the intersection of the Cantor set with a translate of itself is also self-similar. Sufficient and necessary conditions were given by Deng, He, and Wen in 2008. This question has also been generalized to classes of subsets of the unit interval. I plan to discuss how existing ideas can be used to address the question for certain self-similar sets with dimension greater than one. These ideas will be illustrated using a class of self-similar sets in the plane that can be realized as radix expansions in base $-n+i$ where $n$ is a positive integer. I will also discuss a property of the fractal dimensions of these kinds of intersections. </div> </div> <p> <a href="https://www.irif.fr/seminaires/doctorants/index" class="wikilink1" title="seminaires:doctorants:index" data-wiki-id="seminaires:doctorants:index">Séminaire des membres non-permanents</a><br/> Jeudi 20 février 2025, 16 heures, Salle 3052<br/> <strong>Miriam Marzaioli</strong> <em>A Crèche Introduction to Cohen's Forcing</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b12-283"><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="b12-283"><div class="bs-wrap bs-wrap-well well well-sm"> In 1963, Paul Cohen discovered the forcing method and definitively answered the first of Hilbert's 23 problems by using this technique to prove the independence of the Continuum Hypothesis from the ZFC axioms. Since then, forcing has become the primary tool in set theory for establishing independence and consistency results. In this talk, we will present the key ingredients and ideas necessary to understand Cohen's model of ZFC + ¬CH. In particular, we will explore Cohen's forcing via the boolean-valued models approach. </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 21 février 2025, 14 heures, Salle 3052<br/> <strong>Andrew Ryzhikov</strong> (University of Warsaw) <em>How combinatorics stands in the way of matrix reachability (and what we can do about that)</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b5-284"><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-284"><div class="bs-wrap bs-wrap-well well well-sm"> Combinatorial automata theory can be seen as studying reachability in transformation semigroups. An interesting way of generalising this setting is by lifting it up to reachability in finite semigroups of rational matrices. Here, besides finite automata theory, other areas come into play, for example weighted automata, algebraic number theory, and multilinear algebra. I will explain several nice questions (such as mortality and minimum rank) that transfer from transformation semigroups to finite matrix semigroups. I will also explain the lack of mathematical structure that is brought by certain PSPACE-complete transformation semigroup problems. </div> </div> <p> <a href="https://www.irif.fr/seminaires/adg/index" class="wikilink1" title="seminaires:adg:index" data-wiki-id="seminaires:adg:index">Algorithmique distribuée et graphes</a><br/> Mardi 25 février 2025, 15 heures, 3052<br/> <strong>Narges Tavassoli</strong> (CRIStAL, Université de Lille) <em>The Parameterized Complexity of Local Search for MOTSP</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b10-285"><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="b10-285"><div class="bs-wrap bs-wrap-well well well-sm"> This research aims to connect two important areas: parameterized complexity and multi-objective optimization. Parameterized complexity is a way of studying how efficiently an algorithm can solve a problem by focusing on given parameters, while multi-objective optimization focuses on real-world problems that have several goals to achieve at once. The Multi-Objective Traveling Salesman Problem (MOTSP) is a variation of the Traveling Sales-man Problem (TSP) where a salesman must visit a set of cities and return to the starting point, but instead of optimizing just one objective (like minimizing distance), there are multiple objectives to consider simultaneously. These objectives could be things like minimizing total cost, distance, or travel time, while also considering factors like fuel consumption or safety. We aim to solve MOTSP using a local search method. To enhance the effectiveness of this approach, we have proposed a new neighborhood operator. The Local MOTSP(r-swap) problem takes as input an H-ordered graph G = (V, E), two edge weight functions w1, w2 with maximum weight W, and a positive integer k. The goal is to determine whether there exists an ordered sequence S of at most k r-swaps such that perm(S) results in an improved Hamiltonian cycle. The problem is parameterized by r, k and W. We show that even with multiple objectives, the problem can still be solved in FPT time, specifically in time O(k2·k!·r2(k−1)·n + k5·r ·W4·n2). </div> </div> <p> <a href="https://www.irif.fr/seminaires/semantique/index" class="wikilink1" title="seminaires:semantique:index" data-wiki-id="seminaires:semantique:index">Sémantique</a><br/> Mardi 25 février 2025, 15 heures, Salle 3071<br/> <strong>Ariadne Si Suo</strong> (Cambridge) <em>Type Checking is Proof Reductions in Classical Linear Logic</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b15-286"><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="b15-286"><div class="bs-wrap bs-wrap-well well well-sm"> I will try to convince you type checkers can be seen as logic programs with ‘directions’, and doing type checking correspond to proof reductions in classical linear logic. This gives us implementations of type checking algorithms for free, by writing bidirectional typing rules as directional logic programs. If time permits, I will tell you some categorical details, or possible extensions to accommodate more expressive type systems. Based on joint work with Vikraman Choudhury and Neel Krishnaswami. </div> </div> <p> <a href="https://www.irif.fr/seminaires/hors-series/index" class="wikilink1" title="seminaires:hors-series:index" data-wiki-id="seminaires:hors-series:index">Évènement spécial</a><br/> Mercredi 26 février 2025, 9 heures, Amphi Turing, Sophie Germain<br/> <strong>Sam Van Gool</strong> (IRIF & IMJ) <em>Logique à Paris</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b24-287"><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="b24-287"><div class="bs-wrap bs-wrap-well well well-sm"> In collaboration with the logic group of the math department (IMJ-PRG), PPS pole is organizing a meeting: <ul class=" fix-media-list-overlap"> <li class="level1"><div class="li"> Logique à Paris </div> </li> <li class="level1"><div class="li"> <strong>26 - 28 February 2025</strong> </div> </li> <li class="level1"><div class="li"> Amphi Turing, Sophie Germain </div> </li> <li class="level1"><div class="li"> <a href="https://www.sylvyanscombe.com/logiqueaparis2025.html" class="urlextern" title="https://www.sylvyanscombe.com/logiqueaparis2025.html" rel="ugc nofollow">https://www.sylvyanscombe.com/logiqueaparis2025.html</a></div> </li> </ul> <p> Talks are given by six invited speakers on various current topics in logic, which in several cases include interactions with the foundations of computer science: Albert Atserias, Ingo Blechschmidt, Laura Fontanella, Jonathan Kirby, Chris Lambie-Hanson, Mariana Vicaria. </p> <p> Each speaker will give two hours of lectures; typically, the first lecture gives a broad introduction to their domain, followed by a more in-depth talk on a recent topic. </p> <p> If you would like to attend one or more of the talks, we kindly request that you register via the link above. </div> </p> </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 28 février 2025, 14 heures, Salle 3052<br/> <strong>Herman Goulet-Ouellet</strong> <em>Non encore annoncé.</em> </p> </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&1739806028" width="2" height="1" alt="" /> </div> </body> </html>