CINXE.COM

<!DOCTYPE html> <html xmlns="http://www.w3.org/1999/xhtml" lang="en" dir="ltr" class="no-js"> <head> <meta charset="UTF-8" /> <title>Welcome</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="en,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/en/index?do=index" title="Sitemap"/> <link rel="manifest" href="https://www.irif.fr/lib/exe/manifest.php"/> <link rel="alternate" type="text/html" title="Plain HTML" href="https://www.irif.fr/_export/xhtml/en/index"/> <link rel="alternate" type="text/plain" title="Wiki Markup" href="https://www.irif.fr/_export/raw/en/index"/> <link rel="canonical" href="https://www.irif.fr/en/index"/> <link rel="stylesheet" href="https://www.irif.fr/lib/exe/css.php?t=bootstrap3&tseed=68afda03198d2497d21d700ee877901a"/> <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='en';var JSINFO = {"plugin":{"datatables":{"config":{"dom":"lBfrtip","language":{"url":"https:\/\/www.irif.fr\/lib\/plugins\/datatables\/assets\/datatables.net-i18n\/en-GB.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":"en:index","namespace":"en","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=68afda03198d2497d21d700ee877901a&lang=en" 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 dw-fluid-container" data-page-id="en: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">INFORMATION <span class="caret"></span></a> <ul class="dropdown-menu" role="menu"> <li class="level2"> <a href="https://www.irif.fr/en/informations/presentation" class="wikilink1" title="en:informations:presentation" >Presentation</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/informations/contacts" class="wikilink1" title="en:informations:contacts" >Contact and access</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/informations/charte" class="wikilink1" title="en:informations:charte" >IRIF Members Charter</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/egalite-fh/index" class="wikilink1" title="en:egalite-fh:index" >Equality</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/environnement/index" class="wikilink1" title="en:environnement:index" >Environment</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/informations/annuaire" class="wikilink1" title="en:informations:annuaire" >Directory</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/informations/mentorat" class="wikilink1" title="en:informations:mentorat" >IRIF’s mentoring program</a> </li> <li class="level2"> <a href="https://www.irif.fr/informations/childcare" class="wikilink1" title="informations:childcare" >Childcare program</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">RESEARCH <span class="caret"></span></a> <ul class="dropdown-menu" role="menu"> <li class="level2"> <strong><a href="https://www.irif.fr/en/poles/asd/index" class="wikilink1" title="en:poles:asd:index" >Algorithms and discrete structures</a></strong> </li> <li class="level2"> <a href="https://www.irif.fr/en/equipes/algocomp/index" class="wikilink1" title="en:equipes:algocomp:index" >Algorithms and complexity</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/equipes/combi/index" class="wikilink1" title="en:equipes:combi:index" >Combinatorics</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/equipes/distribue/index" class="wikilink1" title="en:equipes:distribue:index" >Distributed computing</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/equipes/graphes/index" class="wikilink1" title="en:equipes:graphes:index" >Theory and algorithmics of graphs</a> </li> <li class="level2"> <strong><a href="https://www.irif.fr/en/poles/asv/index" class="wikilink1" title="en:poles:asv:index" >Automata, structures and verification</a></strong> </li> <li class="level2"> <a href="https://www.irif.fr/en/equipes/automates/index" class="wikilink1" title="en:equipes:automates:index" >Automata and applications</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/equipes/verif/index" class="wikilink1" title="en:equipes:verif:index" >Modeling and verification</a> </li> <li class="level2"> <strong><a href="https://www.irif.fr/en/poles/pps/index" class="wikilink1" title="en:poles:pps:index" >Proofs, programs and systems</a></strong> </li> <li class="level2"> <a href="https://www.irif.fr/en/equipes/algebre/index" class="wikilink1" title="en:equipes:algebre:index" >Algebra and computation</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/equipes/programmes/index" class="wikilink1" title="en:equipes:programmes:index" >Programs and Languages (PL)</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/equipes/preuves/index" class="wikilink1" title="en:equipes:preuves:index" >Proofs and programs</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/equipes/picube/index" class="wikilink1" title="en: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><br/> </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">EVENTS <span class="caret"></span></a> <ul class="dropdown-menu" role="menu"> <li class="level2"> <strong><a href="https://www.irif.fr/en/seminaires/evenements" class="wikilink1" title="en:seminaires:evenements" >IRIF events</a></strong> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/irif/index" class="wikilink1" title="en:seminaires:irif:index" >IRIF Distinguished Talks Series</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/rencontres/irif/index" class="wikilink1" title="en:rencontres:irif:index" >IRIF days</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/rencontres/poles/index" class="wikilink1" title="en:rencontres:poles:index" >Pole meetings</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/env/index" class="wikilink1" title="en:seminaires:env:index" >IRIF and environment group</a> </li> <li class="level2"> <strong><a href="https://www.irif.fr/en/seminaires/seminaires" class="wikilink1" title="en:seminaires:seminaires" >Research seminars</a></strong> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/algocomp/index" class="wikilink1" title="en:seminaires:algocomp:index" >Algorithms and complexity</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/asd/index" class="wikilink1" title="en:seminaires:asd:index" >Algorithms and discrete structures</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/automates/index" class="wikilink1" title="en:seminaires:automates:index" >Automata</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/combi/index" class="wikilink1" title="en:seminaires:combi:index" >Enumerative and analytic combinatorics</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/adg/index" class="wikilink1" title="en:seminaires:adg:index" >Graphs and distributed computing</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/picube/index" class="wikilink1" title="en:seminaires:picube:index" >Formath</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/pps/index" class="wikilink1" title="en:seminaires:pps:index" >Proofs, programs and systems</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/verif/index" class="wikilink1" title="en:seminaires:verif:index" >Verification</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/doctorants/index" class="wikilink1" title="en:seminaires:doctorants:index" >Non-permanent members’ seminar</a> </li> <li class="level2"> <strong><a href="https://www.irif.fr/en/seminaires/onlineseminars" class="wikilink1" title="en:seminaires:onlineseminars" >Online seminars</a></strong> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/greta/index" class="wikilink1" title="en:seminaires:greta:index" >Graph Transformation Theory and Applications</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/numeration/index" class="wikilink1" title="en:seminaires:numeration:index" >One world numeration seminar</a> </li> <li class="level2"> <strong><a href="https://www.irif.fr/en/seminaires/gt" class="wikilink1" title="en:seminaires:gt" >Working groups</a></strong> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/gel/index" class="wikilink1" title="en:seminaires:gel:index" >Graphs and Logic</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/cat/index" class="wikilink1" title="en:seminaires:cat:index" >Higher categories, polygraphs and homotopy</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" >Logic, automata, algebra and games</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/programmation/index" class="wikilink1" title="en:seminaires:programmation:index" >Programming</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/semantique/index" class="wikilink1" title="en:seminaires:semantique:index" >Semantics</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/sms/index" class="wikilink1" title="en:seminaires:sms:index" >Syntax Meets Semantics</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/topos/index" class="wikilink1" title="en:seminaires:topos:index" >Topos Theory</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/hott/index" class="wikilink1" title="en:seminaires:hott:index" >Type theory and homotopy theory</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/types/index" class="wikilink1" title="en:seminaires:types:index" >Type theory and realisability</a> </li> <li class="level2"> <strong><a href="https://www.irif.fr/en/seminaires/soutenances" class="wikilink1" title="en:seminaires:soutenances" >Defences</a></strong> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/these/index" class="wikilink1" title="en:seminaires:these:index" >PhD defences</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/hdr/index" class="wikilink1" title="en:seminaires:hdr:index" >Habilitation defences</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">MEDIATION <span class="caret"></span></a> <ul class="dropdown-menu" role="menu"> <li class="level2"> <a href="https://www.irif.fr/en/mediation/fdls" class="wikilink1" title="en:mediation:fdls" >Fête de la Science</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/mediation/scolaire" class="wikilink1" title="en:mediation:scolaire" >Middle/High school internships</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/portraits/index" class="wikilink1" title="en:portraits:index" >Research profiles</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">50 Years Exhibitation</a> </li> <li class="level2"> <a href="https://qubobs.irif.fr" class="" title="https://qubobs.irif.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">HIGHLIGHTS <span class="caret"></span></a> <ul class="dropdown-menu" role="menu"> <li class="level2"> <a href="https://www.irif.fr/en/distinctions/index" class="wikilink1" title="en:distinctions:index" >Awards and Honors</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/logiciels/index" class="wikilink1" title="en:logiciels:index" >Software</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/contrats/index" class="wikilink1" title="en:contrats:index" >Grants</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/international/index" class="wikilink1" title="en:international:index" >International Collaborations</a> </li> <li class="level2"> <a href="https://epit.irif.fr" class="" title="https://epit.irif.fr" rel="ugc nofollow">The EPIT Research School</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/formation/index" class="wikilink1" title="en:formation:index" >Academics</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">JOIN US <span class="caret"></span></a> <ul class="dropdown-menu" role="menu"> <li class="level2"> <a href="https://www.irif.fr/en/informations/visit" class="wikilink1" title="en:informations:visit" >Visitor program</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/postes/admin" class="wikilink1" title="en:postes:admin" >Research support position</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/postes/universite" class="wikilink1" title="en:postes:universite" >Faculty members</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/postes/chercheur" class="wikilink1" title="en:postes:chercheur" >Researchers</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/postes/postdoc" class="wikilink1" title="en:postes:postdoc" >Postdocs</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/postes/ater" class="wikilink1" title="en:postes:ater" >Teaching assistants</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/postes/these" class="wikilink1" title="en:postes:these" >PhD Studies</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/postes/stage" class="wikilink1" title="en:postes:stage" >Master Internships</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/postes/stage-scolaire" class="wikilink1" title="en:postes:stage-scolaire" >Middle/High school internships</a> </li> </ul> </li> </ul> <ul class="nav navbar-nav"> <li class="level1"> <a href="https://www.irif.fr/en/intranet/index" class="wikilink1" title="en: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="Translations of this 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">Translations of this 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> Translations of this page </li> <li><div class='li'><a href="https://www.irif.fr/index" class="wikilink1 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 cur'><a href="https://www.irif.fr/en/index" class="wikilink1 cur 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/en/index?do=login&sectok=" title="Log In" 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=""> Log In</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="welcome">Welcome</h2> <div class="plugin_include_content plugin_include__en:bienvenue" id="plugin_include__en__bienvenue"> <div class="level0"> <p> IRIF is a research laboratory of <a href="http://www.cnrs.fr" class="urlextern" title="http://www.cnrs.fr" rel="ugc nofollow">CNRS</a> and <a href="http://www.u-paris.fr/" class="urlextern" title="http://www.u-paris.fr/" rel="ugc nofollow">Université Paris Cité</a>, also hosting one <a href="http://www.inria.fr" class="urlextern" title="http://www.inria.fr" rel="ugc nofollow">Inria</a> project-team. </p> <p> The research conducted at IRIF is based on the study and understanding of the foundations of all computer science, in order to provide innovative solutions to the current and future challenges of digital sciences. </p> <p> IRIF hosts about 200 people. Seven of its members have been distinguished by the <a href="https://erc.europa.eu" class="urlextern" title="https://erc.europa.eu" rel="ugc nofollow">European Research Council (ERC)</a>, six are members of <a href="http://www.iufrance.fr" class="urlextern" title="http://www.iufrance.fr" rel="ugc nofollow">the Institut Universitaire de France IUF)</a>, two are members of the <a href="http://www.ae-info.org" class="urlextern" title="http://www.ae-info.org" rel="ugc nofollow">Academia Europæa</a>, and one is member of <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> <p>  </p> <h2 class="sectionedit20 page-header pb-3 mb-4 mt-5" id="notion_of_the_day">Notion of the day</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="social_networks">Social Networks</h2> <p> Follow us on Twitter/X, LinkedIn and Mastodon for our latest news: </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="news">News</h2> <div class="plugin_include_content plugin_include__en:actualites:index" id="plugin_include__en__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/aaai_2025.jpg?id=en%3Aindex" class="media" title="actualites:ressources:aaai_2025.jpg"><img src="https://www.irif.fr/_media/actualites/ressources/aaai_2025.jpg?w=60&tok=33a1d7" class="medialeft img-responsive" loading="lazy" title="aaai_2025.jpg" alt="aaai_2025.jpg" width="60" /></a></span> <p> <em>10.3.2025</em><br/> Congratulations to <a href="https://www.irif.fr/~horn/" class="urlextern" title="https://www.irif.fr/~horn/" rel="ugc nofollow">Florian Horn</a>, co-author of <em>Revelations: A Decidable Class of POMDPs with Omega-Regular Objectives</em>, a paper awarded the “<strong>Outstanding Paper Awards</strong>” at <a href="https://aaai.org/conference/aaai/aaai-25/" class="urlextern" title="https://aaai.org/conference/aaai/aaai-25/" rel="ugc nofollow">AAAI 2025</a>. <a href="https://aihub.org/2025/03/01/congratulations-to-the-aaai2025-outstanding-paper-award-winners/" 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/podcast_geoffroycouteau.jpg?id=en%3Aindex" class="media" title="actualites:ressources:podcast_geoffroycouteau.jpg"><img src="https://www.irif.fr/_media/actualites/ressources/podcast_geoffroycouteau.jpg?w=60&tok=7ddce2" class="medialeft img-responsive" loading="lazy" title="podcast_geoffroycouteau.jpg" alt="podcast_geoffroycouteau.jpg" width="60" /></a></span> <p> <em>14.3.2025</em><br/> The third episode of the CNRS podcast “<a href="https://podcast.ausha.co/cnrs-qu-est-ce-que-tu-cherches" class="urlextern" title="https://podcast.ausha.co/cnrs-qu-est-ce-que-tu-cherches" rel="ugc nofollow">Qu'est-ce que tu cherches ?</a>” features <a href="https://geoffroycouteau.github.io/" class="urlextern" title="https://geoffroycouteau.github.io/" rel="ugc nofollow">Geoffroy Couteau</a>, who <strong>talks about his research</strong> on data privacy protection, secure computations, and secure protocols. You will also get a glimpse into his typical day, the time when he is most productive in science (and no, it's not necessarily during the day!), and the stereotypes associated with his field. (Re)listen to this episode: <a href="https://podcast.ausha.co/cnrs-qu-est-ce-que-tu-cherches/comment-proteger-nos-donnees-privees-geoffroy-couteau-cnrs" 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/flash_opti.png?id=en%3Aindex" class="media" title="actualites:ressources:flash_opti.png"><img src="https://www.irif.fr/_media/actualites/ressources/flash_opti.png?w=60&tok=2470af" class="medialeft img-responsive" loading="lazy" alt="" width="60" /></a></span> <p> <em>18.2.2025</em><br/> For the CNRS conference titled « L’optimisation, au cœur des défis des sciences informatiques » (Optimization, at the core of the challenges of computer science), <a href="https://simonapers.github.io/" class="urlextern" title="https://simonapers.github.io/" rel="ugc nofollow">Simon Apers</a>, a CNRS Research Scientist at IRIF delivered a three-minute Flash'Opti presentation about how <strong>quantum algorithm can help optimisation</strong>. The Flash'Opti presentations are a CNRS original concept designed to <strong>showcase a research topic in just three minutes, using the support of a single image</strong>. Review his speech: <a href="https://www.youtube.com/watch?v=DSKLbKyoEF4" 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=en%3Aindex" 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> has published a new book on the <strong>history of calculation, titled 𝐿𝑒 𝑐𝑎𝑙𝑐𝑢𝑙 𝑎̀ 𝑑𝑒́𝑐𝑜𝑢𝑣𝑒𝑟𝑡</strong>. Several current and former IRIF researchers contributed to the writing of this book by authoring chapters: <br/> ◻️ Part 4: ▪️ Chapter 1 - 𝑳'𝒂𝒍𝒈𝒐𝒓𝒊𝒕𝒉𝒎𝒆 : 𝒗𝒆𝒓𝒔 𝒍𝒂 𝒓𝒆́𝒔𝒐𝒍𝒖𝒕𝒊𝒐𝒏 𝒄𝒐𝒏𝒄𝒓𝒆̀𝒕𝒆 𝒅𝒆 𝒑𝒓𝒐𝒃𝒍𝒆̀𝒎𝒆𝒔 – <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/> ▪️ Chapter 2 - 𝑳𝒂 𝒄𝒐𝒎𝒑𝒍𝒆𝒙𝒊𝒕𝒆́ 𝒂𝒍𝒈𝒐𝒓𝒊𝒕𝒉𝒎𝒊𝒒𝒖𝒆 – <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/> ◻️ Part 9: ▪️ Chapter 1 - 𝑳𝒆𝒔 𝒇𝒐𝒏𝒅𝒆𝒎𝒆𝒏𝒕𝒔 𝒅𝒖 𝒄𝒂𝒍𝒄𝒖𝒍 𝒒𝒖𝒂𝒏𝒕𝒊𝒒𝒖𝒆 – <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/stoc_2025.jpg?id=en%3Aindex" 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/> Congratulations to the <a href="https://www.adrianvladu.org/" class="urlextern" title="https://www.adrianvladu.org/" rel="ugc nofollow">Adrian Vladu</a>, IRIF member, whose <strong>paper have been accepted to STOC 2025</strong>, an ACM conference: <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/flash_opti.png?id=en%3Aindex" class="media" title="actualites:ressources:flash_opti.png"><img src="https://www.irif.fr/_media/actualites/ressources/flash_opti.png?w=60&tok=2470af" class="medialeft img-responsive" loading="lazy" alt="" width="60" /></a></span> <p> <em>18.2.2025</em><br/> For the CNRS conference titled « L’optimisation, au cœur des défis des sciences informatiques » (Optimization, at the core of the challenges of computer science), <a href="http://www.normalesup.org/~saulpic/" class="urlextern" title="http://www.normalesup.org/~saulpic/" rel="ugc nofollow">David Saulpic</a>, a CNRS Research Scientist at IRIF delivered a three-minute Flash'Opti presentation about <strong>Big Data</strong>. The Flash'Opti presentations are a CNRS original concept designed to <strong>showcase a research topic in just three minutes, using the support of a single image</strong>. Take another look at his intervention: <a href="https://www.youtube.com/watch?v=5DADeEhrHMU" 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/science_viejunior_slaplante.png?id=en%3Aindex" class="media" title="actualites:ressources:science_viejunior_slaplante.png"><img src="https://www.irif.fr/_media/actualites/ressources/science_viejunior_slaplante.png?w=60&tok=0f90c8" class="medialeft img-responsive" loading="lazy" alt="" width="60" /></a></span> <p> <em>17.2.2025</em><br/> Science popularization for all ages! <a href="https://www.irif.fr/~laplante/" class="urlextern" title="https://www.irif.fr/~laplante/" rel="ugc nofollow">Sophie Laplante</a>, professor at IRIF, contributed to <strong>issue 425 of Science & Vie Junior</strong>, which features an article on <strong>quantum science</strong>. After an introductory comic, it's time for clear explanations to better understand the <strong>quantum computer and demystify its promises</strong>. Encryption, keys, data, computations, and bits… These concepts are presented in an accessible way, allowing everyone, young and old, to explore the mysteries of quantum science with ease! Discover it in Science & Vie! <a href="https://www.kiosquemag.com/titres/science-vie-junior/sommaire/425" 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/en/actualites/all" class="wikilink1" title="en:actualites:all" data-wiki-id="en:actualites:all">all the past news</a></span> </p> </div> <p> (These news are displayed using a randomized-priority ranking.) </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__en:agenda" id="plugin_include__en__agenda"> <div class="plugin_include_content plugin_include__en:seminaires:weekseminars" id="plugin_include__en__seminaires__weekseminars"> <p> <a href="https://www.irif.fr/en/seminaires/adg/index" class="wikilink1" title="en:seminaires:adg:index" data-wiki-id="en:seminaires:adg:index">Distributed algorithms and graphs</a><br/> Tuesday April 8, 2025, 3:30PM, 3052<br/> <strong>Laurent Viennot</strong> (INRIA et IRIF) <em>Certificates in P and Subquadratic-Time Computation of Radius, Diameter, and all Eccentricities in Graphs</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b10-4633"><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-4633"><div class="bs-wrap bs-wrap-well well well-sm"> In the context of fine-grained complexity, we investigate the notion of certificate enabling faster polynomial-time algorithms. We specifically target radius (minimum eccentricity), diameter (maximum eccentricity), and all-eccentricity computations for which quadratic-time lower bounds are known under plausible conjectures. In each case, we introduce a notion of certificate as a specific set of nodes from which appropriate bounds on all eccentricities can be derived in subquadratic time when this set has sublinear size. The existence of small certificates for radius, diameter and all eccentricities is a barrier against SETH-based lower bounds for these problems. We indeed prove that for graph classes with certificates of bounded size, there exist randomized subquadratic-time algorithms for computing the radius, the diameter, and all eccentricities respectively. Moreover, these notions of certificates are tightly related to algorithms probing the graph through one-to-all distance queries and allow to explain the efficiency of practical radius and diameter algorithms from the literature. </div> </div> <p> <a href="https://www.irif.fr/en/seminaires/pps/index" class="wikilink1" title="en:seminaires:pps:index" data-wiki-id="en:seminaires:pps:index">Proofs, programs and systems</a><br/> Thursday April 10, 2025, 10:30AM, Salle 3052 & online (<a href="https://u-paris.zoom.us/j/84381797685?pwd=WG1ZSnhnYi81MnhsTFB6S2krM0E2Zz09" class="urlextern" title="https://u-paris.zoom.us/j/84381797685?pwd=WG1ZSnhnYi81MnhsTFB6S2krM0E2Zz09" rel="ugc nofollow">Zoom link</a>)<br/> <strong>Justin Hsu</strong> (Cornell University) <em>Type Systems for Numerical Error Analysis</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b4-4634"><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="b4-4634"><div class="bs-wrap bs-wrap-well well well-sm"> Programs in numerical analysis and scientific computing make heavy use of floating-point numbers to approximate ideal real numbers. Operations on floating-point numbers incur roundoff error, and an important practical problem is to bound the overall magnitude of the error for complex computations. Existing work employs a variety of strategies such as interval arithmetic, SMT encodings, and global optimization; however, current methods are not compositional and are limited in scalability, precision, and expressivity. <p> Today, I'll talk about some of our recent work on NumFuzz, a higher-order language that can bound forward error using a linear, coeffect type system for sensitivity analysis combined with a novel quantitative error type. Our type inference procedure can derive precise relative error bounds for programs that are several orders of magnitude larger than previously possible. </p> <p> If time permits, I'll briefly discuss a second type system called Bean for bounding backward error. Like NumFuzz, Bean is based on a linear coeffect type system, but it features a semantics based on a novel category of lenses on metric spaces. Bean is the first system to soundly reason about backward error in numerical programs. </p> <p> Joint work with Ariel Kellison, Laura Zielinski, and David Bindel. </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/doctorants/index" class="wikilink1" title="en:seminaires:doctorants:index" data-wiki-id="en:seminaires:doctorants:index">Non-permanent members' seminar</a><br/> Thursday April 10, 2025, 4PM, Salle 3052<br/> <strong>Vincent Moreau</strong> <em>To be announced.</em> </p> <p> <a href="https://www.irif.fr/en/seminaires/automates/index" class="wikilink1" title="en:seminaires:automates:index" data-wiki-id="en:seminaires:automates:index">Automata</a><br/> Friday April 11, 2025, 2PM, Salle 3052<br/> <strong>Mahsa Shirmohammadi</strong> <em>Differential Tree Automata</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b5-4635"><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-4635"><div class="bs-wrap bs-wrap-well well well-sm"> A rationally dynamically algebraic (RDA) power series is one that arises as (a component of) the solution of a system of differential equations of the form y′=F(y), where F is a vector of rational functions that is defined at y(0). RDA power series subsume algebraic power series and are a proper subclass of differentially algebraic power series (those that satisfy a univariate polynomial-differential equation). We give a combinatorial characterisation of RDA power series in terms of exponential generating functions of regular languages of labelled trees. Motivated by this connection, we define the notion of a differential tree automaton. Differential tree automata generalise weighted tree automata by allowing the transition weights to be rational functions of the tree size. Our main result is that the ordinary generating functions of the formal tree series recognised by differential tree automata are exactly the differentially algebraic power series. The proof of this result establishes a general form of recurrence satisfied by the sequence of coefficients of a differentially algebraic power series, generalising Reutenauer's matrix representation of polynomially recursive sequences. As a corollary we obtain a procedure for determining equality of differential tree automata. <p> The talk is based on a joint work with Rida Ait El Manssour, Vincent Cheval, and James Worrell and can be found here: <a href="https://arxiv.org/abs/2407.08218" class="urlextern" title="https://arxiv.org/abs/2407.08218" rel="ugc nofollow">https://arxiv.org/abs/2407.08218</a> </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/verif/index" class="wikilink1" title="en:seminaires:verif:index" data-wiki-id="en:seminaires:verif:index">Verification</a><br/> Friday April 11, 2025, 11AM, 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>Marc Shapiro</strong> (LIP6, Sorbonne Université) <em>Modelling and Verifying a Database Backend</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b11-4636"><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-4636"><div class="bs-wrap bs-wrap-well well well-sm"> Although a database backing store is conceptually just a shared memory, modern stores have high internal complexity, for performance and fault tolerance reasons, and to support rich data types supporting incremental and/or convergent updates. As such complexity is bug-prone, this research proposes a correct-by-design approach, based on a set of formal specifications. <p> Possible executions are abstracted as a trace, a partial order of transactional events. Its valuation specifies the expected value of a key at each event, according to datatype semantics. </p> <p> We specify two common variants of store, the eager, random-access map and the lazy, sequential-access journal. We show that both conform to the valuation, meaning that they are (i) safe, (ii) functionally equivalent, and (iii) causally consistent. </p> <p> Finally, we propose a transaction semantics that is representative of common implementations and avoids the timestamp inversion anomaly. We show an equivalence between the trace and the transaction semantics; implying that maps and journals remain safe. Our results extend naturally to systems with stronger guarantees, such as classical assignment-based data types or strong consistency. </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/adg/index" class="wikilink1" title="en:seminaires:adg:index" data-wiki-id="en:seminaires:adg:index">Distributed algorithms and graphs</a><br/> Tuesday April 15, 2025, 3PM, 3052<br/> <strong>Florian Horn</strong> (IRIF) <em>To be announced.</em> </p> <p> <a href="https://www.irif.fr/en/seminaires/pps/index" class="wikilink1" title="en:seminaires:pps:index" data-wiki-id="en:seminaires:pps:index">Proofs, programs and systems</a><br/> Thursday April 17, 2025, 10:30AM, Salle 3052<br/> <strong>Hector Suzanne</strong> (LIP6 (Sorbonne Université)) <em>Reusable resource analysis for high-level languages</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b4-4637"><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="b4-4637"><div class="bs-wrap bs-wrap-well well well-sm"> Static resource analysis is dedicated to finding methods to determine the quantity of resources (time, energy, memory, …) required to run a program, together with the variables this quantity depends on. The cornerstone of this endeavor is finding invariants/variants between program states: an analyser must automatically understand the algorithms encoded into the program without programmer input. <p> We focus on resource analyses through type systems for functional languages. To this aim, we introduce AutoBill, an abstract machine used as intermediate representation for resource analysis, based on the lambda-mu-mutilde calculus. We compile to this machine, amongst others, an ML-style language with data-structures (ADT), recursion (fixpoints), and some further extensions. </p> <p> AutoBill uses Call-by-Push-Value operational semantics, which mixes call-by-value and call-by-name, to encode the runtime semantics of functional languages. The use of an abstract machine furthermore allows continuations to be encoded as explicit call stacks. This in turns enables the re-use of data structures analyses to analyse control flow within programs. </p> <p> On top of our machine, a linear type system explicits the resource flow that accompanies jumping in and out of computations. Those types are enriched with integer parameters, that are controlled during type-checking through the addition of equations and constraints to data-type definitions. This enables the approximating sizes, costs, combinatorial invariant, etc. in a first-order constraint, and provides a link between those quantities and the largest resource usage occurring at runtime. This is done during type-inference, and the constraint is then sent to an SMT solver for validation, or to a linear programming optimizer to generate resource bounds. </p> <p> We implement the “Automated Amortized Resource Analysis” method in AutoBill. It assigns, to each data-structure, a count of the amount of sub-structures with some relevant shape. This is then used to bound the iteration counts of an algorithm and obtain polynomial worst-case complexities. Our implementation consists of a specialized compilation scheme from a source language to the abstract machine. The typing-and-analysis engine is then independent of both the source language and the chosen analysis method. </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/adg/index" class="wikilink1" title="en:seminaires:adg:index" data-wiki-id="en:seminaires:adg:index">Distributed algorithms and graphs</a><br/> Tuesday April 22, 2025, 3PM, 3052<br/> <strong>Fabien De Montgolfier</strong> (IRIF) <em>Beating LexBFS with BFS and DFS</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b10-4638"><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-4638"><div class="bs-wrap bs-wrap-well well well-sm"> In this talk I will present a work in progress : how simple graph searches such as Depth First Search (DFS) or Breadth First Search (BFS) can be used to recognize simple structured classes of graphs. For these three classes, Trivially Perfect graphs, Proper Interval graphs (aka Unit Interval Graphs), and Chordal graphs, the simplest (among linear-time) known algorithms use LexBFS instead (applied once or thrice). </div> </div> <p> <a href="https://www.irif.fr/en/seminaires/algocomp/index" class="wikilink1" title="en:seminaires:algocomp:index" data-wiki-id="en:seminaires:algocomp:index">Algorithms and complexity</a><br/> Wednesday April 23, 2025, 11AM, Salle 3052<br/> <strong>Lennart Braun</strong> (IRIF) <em>Low-Bandwidth Mixed Arithmetic in VOLE-Based Zero-Knowledge from Low-Degree PRGs</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b9-4639"><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="b9-4639"><div class="bs-wrap bs-wrap-well well well-sm"> Vector oblivious linear evaluation, or VOLE, has recently been shown to be a useful tool for designing efficient zero-knowledge proof systems that can scale to large statements with a low memory footprint (Yang et al. CCS 2021, Baum et al. CRYPTO 2021). While most ZK protocols require statements to be expressed in terms of arithmetic operations over a single finite field, recent works in VOLE-based ZK have shown how to mix Boolean and arithmetic operations in a single statement, through conversions between different finite fields (Baum et al. CCS 2021, Weng et al. USENIX 2021). <p> We present new, lightweight protocols for arithmetic/Boolean conversions in VOLE-based ZK. In contrast to previous works, which rely on an expensive cut-and-choose method, we take a new approach that leverages the ability of recent proof systems to prove high-degree polynomial constraints, and combines this with specialized low-degree pseudorandom generators. This not only simplifies conversions, but we showcase how it also improves the concrete efficiency of tasks important in practical ZK protocols of complex statements, including fixed point arithmetic, comparison and range proofs. </p> <p> Joint work with Amit Agarwal (currently visiting IRIF), Carsten Baum, and Peter Scholl. To be presented at Eurocrypt 2025. </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/verif/index" class="wikilink1" title="en:seminaires:verif:index" data-wiki-id="en:seminaires:verif:index">Verification</a><br/> Monday April 28, 2025, 11AM, 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>Radu Iosif</strong> (VERIMAG, Université Grenoble Alpes) <em>Regular Grammars for Sets of Graphs of Tree-Width 2</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b11-4640"><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-4640"><div class="bs-wrap bs-wrap-well well well-sm"> Regular word grammars are context-free grammars having restricted rules, that define all recognizable languages of words. This paper generalizes regular grammars from words to certain classes of graphs, by defining regular grammars for unordered unranked trees and graphs of tree-width 2 at most. The qualifier ``regular'' is justified because these grammars define precisely the recognizable (equivalently, CMSO-definable) sets of the respective graph classes. The proof of equivalence between regular and recognizable sets of graphs relies on the effective construction of a recognizer algebra of size doubly-exponential in the size of the grammar. This sets a 2EXPTIME upper bound on the (EXPTIME-hard) problem of inclusion of a context-free language in a regular language, for graphs of tree-width 2 at most. A further syntactic restriction of regular grammars suffices to capture precisely the MSO-definable sets of graphs of tree-width 2 at most, i.e., the sets defined by CMSO formulae without cardinality constraints. Moreover, we show that MSO-definability coincides with recognizability by algebras having an aperiodic parallel composition semigroup, for each class of graphs defined by a bound on the tree-width. </div> </div></div> </div> </div><div class="wrap_clear plugin_wrap"></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="skip to content" 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=en%3Aindex&1743943441" width="2" height="1" alt="" /> </div> </body> </html>