CINXE.COM

<!DOCTYPE html> <html xmlns="http://www.w3.org/1999/xhtml" lang="fr" dir="ltr" class="no-js"> <head> <meta charset="UTF-8" /> <title>Journées PPS 2021</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="rencontres,pps2021,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/rencontres/pps2021/index?do=index" title="Plan du site"/> <link rel="manifest" href="https://www.irif.fr/lib/exe/manifest.php"/> <link rel="alternate" type="text/html" title="HTML brut" href="https://www.irif.fr/_export/xhtml/rencontres/pps2021/index"/> <link rel="alternate" type="text/plain" title="Wiki balise" href="https://www.irif.fr/_export/raw/rencontres/pps2021/index"/> <link rel="canonical" href="https://www.irif.fr/rencontres/pps2021/index"/> <link rel="stylesheet" href="https://www.irif.fr/lib/exe/css.php?t=bootstrap3&tseed=999b1f07158911a883ed4b945a522775"/> <link type="text/css" rel="stylesheet" href="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net-fixedheader-dt/css/fixedHeader.dataTables.min.css"/> <link type="text/css" rel="stylesheet" href="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net-fixedcolumns-dt/css/fixedColumns.dataTables.min.css"/> <link type="text/css" rel="stylesheet" href="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net/css/dataTables.bootstrap.min.css"/> <link type="text/css" rel="stylesheet" href="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net-buttons/css/buttons.bootstrap.min.css"/> <link type="text/css" rel="stylesheet" href="https://www.irif.fr/lib/plugins/icons/assets/font-awesome/css/font-awesome.min.css"/> <link type="text/css" rel="stylesheet" href="https://www.irif.fr/lib/plugins/icons/assets/material-design-icons/css/materialdesignicons.min.css"/>  <script >/*<![CDATA[*/var NS='rencontres:pps2021';var JSINFO = {"plugin":{"datatables":{"config":{"dom":"lBfrtip","language":{"url":"https:\/\/www.irif.fr\/lib\/plugins\/datatables\/assets\/datatables.net-i18n\/fr-FR.json"}},"enableForAllTables":1}},"move_renameokay":false,"move_allowrename":false,"bootstrap3":{"mode":"show","toc":[],"config":{"collapsibleSections":0,"fixedTopNavbar":1,"showSemanticPopup":0,"sidebarOnNavbar":1,"tagsOnTop":1,"tocAffix":1,"tocCollapseOnScroll":1,"tocCollapsed":0,"tocLayout":"default","useAnchorJS":1,"useAlternativeToolbarIcons":1}},"id":"rencontres:pps2021:index","namespace":"rencontres:pps2021","ACT":"show","useHeadingNavigation":1,"useHeadingContent":1}; /*!]]>*/</script> <script src="https://www.irif.fr/lib/exe/jquery.php?tseed=34a552433bc33cc9c3bc32527289a0b2" defer="defer"></script> <script src="https://www.irif.fr/lib/exe/js.php?t=bootstrap3&tseed=999b1f07158911a883ed4b945a522775" defer="defer"></script> <script type="text/javascript" src="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net/js/jquery.dataTables.min.js" defer="defer"></script> <script type="text/javascript" src="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net-fixedheader-dt/js/fixedHeader.dataTables.min.js" defer="defer"></script> <script type="text/javascript" src="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net-fixedcolumns-dt/js/fixedColumns.dataTables.min.js" defer="defer"></script> <script type="text/javascript" src="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net-buttons/js/dataTables.buttons.min.js" defer="defer"></script> <script type="text/javascript" src="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net-buttons/js/buttons.html5.min.js" defer="defer"></script> <script type="text/javascript" src="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net-buttons/js/buttons.print.min.js" defer="defer"></script> <script type="text/javascript" src="https://www.irif.fr/lib/plugins/datatables/assets/jszip/jszip.min.js" defer="defer"></script> <script type="text/javascript" src="https://www.irif.fr/lib/plugins/datatables/assets/pdfmake/pdfmake.min.js" defer="defer"></script> <script type="text/javascript" src="https://www.irif.fr/lib/plugins/datatables/assets/pdfmake/vfs_fonts.js" defer="defer"></script> <script type="text/javascript" src="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net/js/dataTables.bootstrap.min.js" defer="defer"></script> <script type="text/javascript" src="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net-buttons/js/buttons.bootstrap.min.js" defer="defer"></script> <script type="text/x-mathjax-config">/*<![CDATA[*/MathJax.Hub.Config({ tex2jax: { inlineMath: [ ["$","$"], ["\$","\$"] ], displayMath: [ ["$$","$$"], ["\\[","\\]"] ], processEscapes: true } }); /*!]]>*/</script> <script type="text/javascript" charset="utf-8" src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.9/MathJax.js?config=TeX-AMS_CHTML.js"></script>  <style type="text/css">@media screen { body { margin-top: 60px; } #dw__toc.affix { top: 50px; position: fixed !important; } #dw__toc .nav .nav .nav { display: none; } }</style>  </head> <body class="simplex dokuwiki mode_show tpl_bootstrap3 dw-fluid-container" data-page-id="rencontres:pps2021:index"><div class="dokuwiki"> <header id="dokuwiki__header" class="dw-container dokuwiki container-fluid mx-5">  <nav id="dw__navbar" class="navbar navbar-fixed-top navbar-inverse" role="navigation"> <div class="dw-container container-fluid mx-5"> <div class="navbar-header"> <button class="navbar-toggle" type="button" data-toggle="collapse" data-target=".navbar-collapse"> <span class="icon-bar"></span> <span class="icon-bar"></span> <span class="icon-bar"></span> </button> <a class="navbar-brand d-flex align-items-center" href="https://www.irif.fr/index" accesskey="h" title=""><img id="dw__logo" class="pull-left h-100 mr-4" alt="" src="https://www.irif.fr/_media/logo.png" /><div class="pull-right"><div id="dw__title"></div></div></a> </div> <div class="collapse navbar-collapse"> <ul class="nav navbar-nav"> <li class="level1 node dropdown"><a href="#" class="dropdown-toggle" data-target="#" data-toggle="dropdown" role="button" aria-haspopup="true" aria-expanded="false">INFORMATIONS <span class="caret"></span></a> <ul class="dropdown-menu" role="menu"> <li class="level2"> <a href="https://www.irif.fr/informations/presentation" class="wikilink1" title="informations:presentation" >Présentation</a> </li> <li class="level2"> <a href="https://www.irif.fr/informations/contacts" class="wikilink1" title="informations:contacts" >Contacts et accès</a> </li> <li class="level2"> <a href="https://www.irif.fr/informations/charte" class="wikilink1" title="informations:charte" >Charte des membres de l’IRIF</a> </li> <li class="level2"> <a href="https://www.irif.fr/egalite-fh/index" class="wikilink1" title="egalite-fh:index" >Égalités</a> </li> <li class="level2"> <a href="https://www.irif.fr/environnement/index" class="wikilink1" title="environnement:index" >Environment</a> </li> <li class="level2"> <a href="https://www.irif.fr/informations/annuaire" class="wikilink1" title="informations:annuaire" >Annuaire</a> </li> <li class="level2"> <a href="https://www.irif.fr/informations/mentorat" class="wikilink1" title="informations:mentorat" >Programme de mentorat</a> </li> <li class="level2"> <a href="https://www.irif.fr/informations/childcare" class="wikilink1" title="informations:childcare" >Childcare program</a> </li> <li class="level2"> <a href="https://www.irif.fr/informations/hceres" class="wikilink1" title="informations:hceres" >Évaluation HCERES - 28 au 30 Novembre 2023 (vague D)</a> </li> </ul> </li> </ul> <ul class="nav navbar-nav"> <li class="level1 node dropdown"><a href="#" class="dropdown-toggle" data-target="#" data-toggle="dropdown" role="button" aria-haspopup="true" aria-expanded="false">RECHERCHE <span class="caret"></span></a> <ul class="dropdown-menu" role="menu"> <li class="level2"> <strong><a href="https://www.irif.fr/poles/asd/index" class="wikilink1" title="poles:asd:index" >Algorithmes et structures discrètes</a></strong> </li> <li class="level2"> <a href="https://www.irif.fr/equipes/algocomp/index" class="wikilink1" title="equipes:algocomp:index" >Algorithmes et complexité</a> </li> <li class="level2"> <a href="https://www.irif.fr/equipes/distribue/index" class="wikilink1" title="equipes:distribue:index" >Calcul distribué</a> </li> <li class="level2"> <a href="https://www.irif.fr/equipes/combi/index" class="wikilink1" title="equipes:combi:index" >Combinatoire</a> </li> <li class="level2"> <a href="https://www.irif.fr/equipes/graphes/index" class="wikilink1" title="equipes:graphes:index" >Théorie et algorithmique des graphes</a> </li> <li class="level2"> <strong><a href="https://www.irif.fr/poles/asv/index" class="wikilink1" title="poles:asv:index" >Automates, structures et vérification</a></strong> </li> <li class="level2"> <a href="https://www.irif.fr/equipes/automates/index" class="wikilink1" title="equipes:automates:index" >Automates et applications</a> </li> <li class="level2"> <a href="https://www.irif.fr/equipes/verif/index" class="wikilink1" title="equipes:verif:index" >Modélisation et vérification</a> </li> <li class="level2"> <strong><a href="https://www.irif.fr/poles/pps/index" class="wikilink1" title="poles:pps:index" >Preuves, programmes et systèmes</a></strong> </li> <li class="level2"> <a href="https://www.irif.fr/equipes/algebre/index" class="wikilink1" title="equipes:algebre:index" >Algèbre et calcul</a> </li> <li class="level2"> <a href="https://www.irif.fr/equipes/programmes/index" class="wikilink1" title="equipes:programmes:index" >Programmes et Langages (PL)</a> </li> <li class="level2"> <a href="https://www.irif.fr/equipes/preuves/index" class="wikilink1" title="equipes:preuves:index" >Preuves et programmes</a> </li> <li class="level2"> <a href="https://www.irif.fr/equipes/picube/index" class="wikilink1" title="equipes:picube:index" >Picube (Inria)</a> <hr/> </li> <li class="level2"> <strong><a href="https://cnrs.hal.science/IRIF/" class="" title="https://cnrs.hal.science/IRIF/" rel="ugc nofollow">PUBLICATIONS (hal)</a></strong> </li> </ul> </li> </ul> <ul class="nav navbar-nav"> <li class="level1 node dropdown"><a href="#" class="dropdown-toggle" data-target="#" data-toggle="dropdown" role="button" aria-haspopup="true" aria-expanded="false">ÉVÉNEMENTS <span class="caret"></span></a> <ul class="dropdown-menu" role="menu"> <li class="level2"> <strong><a href="https://www.irif.fr/seminaires/evenements" class="wikilink1" title="seminaires:evenements" >Evénements de l'IRIF</a></strong> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/irif/index" class="wikilink1" title="seminaires:irif:index" >IRIF Distinguished Talks Series</a> </li> <li class="level2"> <a href="https://www.irif.fr/rencontres/irif/index" class="wikilink1" title="rencontres:irif:index" >Journées de l'IRIF</a> </li> <li class="level2"> <a href="https://www.irif.fr/rencontres/poles/index" class="wikilink1" title="rencontres:poles:index" >Rencontres de pôles</a> </li> <li class="level2"> <strong><a href="https://www.irif.fr/seminaires/seminaires" class="wikilink1" title="seminaires:seminaires" >Séminaires de recherche</a></strong> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/algocomp/index" class="wikilink1" title="seminaires:algocomp:index" >Algorithmes et complexité</a> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/asd/index" class="wikilink1" title="seminaires:asd:index" >Algorithmes et structures discrètes</a> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/automates/index" class="wikilink1" title="seminaires:automates:index" >Automates</a> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/combi/index" class="wikilink1" title="seminaires:combi:index" >Combinatoire énumérative et analytique</a> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/picube/index" class="wikilink1" title="seminaires:picube:index" >Séminaire Formath (Formalized Mathematics)</a> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/adg/index" class="wikilink1" title="seminaires:adg:index" >Graphes et calcul distribué</a> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/pps/index" class="wikilink1" title="seminaires:pps:index" >Preuves, programmes et systèmes</a> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/verif/index" class="wikilink1" title="seminaires:verif:index" >Vérification</a> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/doctorants/index" class="wikilink1" title="seminaires:doctorants:index" >Séminaire des membres non-permanents</a> </li> <li class="level2"> <strong><a href="https://www.irif.fr/seminaires/onlineseminars" class="wikilink1" title="seminaires:onlineseminars" >Séminaires en ligne</a></strong> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/greta/index" class="wikilink1" title="seminaires:greta:index" >Graph Transformation Theory and Applications</a> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/numeration/index" class="wikilink1" title="seminaires:numeration:index" >One world numeration seminar</a> </li> <li class="level2"> <strong><a href="https://www.irif.fr/seminaires/gt" class="wikilink1" title="seminaires:gt" >Groupes de travail</a></strong> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/cat/index" class="wikilink1" title="seminaires:cat:index" >Catégories supérieures, polygraphes et homotopie</a> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/sms/index" class="wikilink1" title="seminaires:sms:index" >La syntaxe rencontre la sémantique</a> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/hott/index" class="wikilink1" title="seminaires:hott:index" >La théorie des types et la théorie de l'homotopie</a> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/laag/index" class="wikilink1" title="seminaires:laag:index" >Logique, automates, algèbre et jeux</a> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/programmation/index" class="wikilink1" title="seminaires:programmation:index" >Programmation</a> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/semantique/index" class="wikilink1" title="seminaires:semantique:index" >Sémantique</a> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/types/index" class="wikilink1" title="seminaires:types:index" >Théorie des types et réalisabilité</a> </li> <li class="level2"> <strong><a href="https://www.irif.fr/seminaires/soutenances" class="wikilink1" title="seminaires:soutenances" >Soutenances</a></strong> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/these/index" class="wikilink1" title="seminaires:these:index" >Soutenances de thèses</a> </li> <li class="level2"> <a href="https://www.irif.fr/seminaires/hdr/index" class="wikilink1" title="seminaires:hdr:index" >Soutenances d'habilitation</a> </li> </ul> </li> </ul> <ul class="nav navbar-nav"> <li class="level1 node dropdown"><a href="#" class="dropdown-toggle" data-target="#" data-toggle="dropdown" role="button" aria-haspopup="true" aria-expanded="false">MÉDIATION <span class="caret"></span></a> <ul class="dropdown-menu" role="menu"> <li class="level2"> <a href="https://www.irif.fr/mediation/fdls" class="wikilink1" title="mediation:fdls" >Fête de la Science</a> </li> <li class="level2"> <a href="https://www.irif.fr/mediation/confcrypto" class="wikilink1" title="mediation:confcrypto" >Conférence vidéo “Manuel de Cryptanalyse à l’usage de la NSA”</a> </li> <li class="level2"> <a href="https://www.irif.fr/mediation/scolaire" class="wikilink1" title="mediation:scolaire" >Stages scolaires d’observation</a> </li> <li class="level2"> <a href="https://www.irif.fr/portraits/index" class="wikilink1" title="portraits:index" >Portraits de recherche</a> </li> <li class="level2"> <a href="https://icalp2022.irif.fr/?page_id=1111" class="" title="https://icalp2022.irif.fr/?page_id=1111" rel="ugc nofollow">Exposition 50 ans</a> </li> <li class="level2"> <a href="https://qubobs.irif.fr/fr/" class="" title="https://qubobs.irif.fr/fr/" rel="ugc nofollow">Projet QuBOBS (quantum computing explained)</a> </li> </ul> </li> </ul> <ul class="nav navbar-nav"> <li class="level1 node dropdown"><a href="#" class="dropdown-toggle" data-target="#" data-toggle="dropdown" role="button" aria-haspopup="true" aria-expanded="false">POINTS CLÉS <span class="caret"></span></a> <ul class="dropdown-menu" role="menu"> <li class="level2"> <a href="https://www.irif.fr/distinctions/index" class="wikilink1" title="distinctions:index" > Prix et distinctions</a> </li> <li class="level2"> <a href="https://www.irif.fr/logiciels/index" class="wikilink1" title="logiciels:index" >Logiciels</a> </li> <li class="level2"> <a href="https://www.irif.fr/contrats/index" class="wikilink1" title="contrats:index" >Contrats</a> </li> <li class="level2"> <a href="https://www.irif.fr/international/index" class="wikilink1" title="international:index" >Collaborations internationales</a> </li> <li class="level2"> <a href="https://epit.irif.fr" class="" title="https://epit.irif.fr" rel="ugc nofollow">L'école thématique EPIT</a> </li> <li class="level2"> <a href="https://www.irif.fr/formation/index" class="wikilink1" title="formation:index" >Formation</a> </li> </ul> </li> </ul> <ul class="nav navbar-nav"> <li class="level1 node dropdown"><a href="#" class="dropdown-toggle" data-target="#" data-toggle="dropdown" role="button" aria-haspopup="true" aria-expanded="false">REJOIGNEZ-NOUS <span class="caret"></span></a> <ul class="dropdown-menu" role="menu"> <li class="level2"> <a href="https://www.irif.fr/informations/visit" class="wikilink1" title="informations:visit" >Programme visiteurs</a> </li> <li class="level2"> <a href="https://www.irif.fr/postes/admin" class="wikilink1" title="postes:admin" >Postes soutien à la recherche</a> </li> <li class="level2"> <a href="https://www.irif.fr/postes/universite" class="wikilink1" title="postes:universite" >Enseignant·e·s-chercheurs·euses</a> </li> <li class="level2"> <a href="https://www.irif.fr/postes/chercheur" class="wikilink1" title="postes:chercheur" >Chercheurs·euses</a> </li> <li class="level2"> <a href="https://www.irif.fr/postes/postdoc" class="wikilink1" title="postes:postdoc" >Postdocs</a> </li> <li class="level2"> <a href="https://www.irif.fr/postes/ater" class="wikilink1" title="postes:ater" >ATER</a> </li> <li class="level2"> <a href="https://www.irif.fr/postes/these" class="wikilink1" title="postes:these" >Thèses</a> </li> <li class="level2"> <a href="https://www.irif.fr/postes/stage" class="wikilink1" title="postes:stage" >Stages de master</a> </li> <li class="level2"> <a href="https://www.irif.fr/postes/stage-scolaire" class="wikilink1" title="postes:stage-scolaire" >Stages scolaires d’observation</a> </li> </ul> </li> </ul> <ul class="nav navbar-nav"> <li class="level1"> <a href="https://www.irif.fr/intranet/index" class="wikilink1" title="intranet:index" >INTRANET</a> </li> </ul> <div class="navbar-right" id="dw__navbar_items">  <ul class="nav navbar-nav" id="dw__translation"> <li class="dropdown"> <a href="" class="dropdown-toggle" data-target="#" data-toggle="dropdown" title="Traductions de cette page" role="button" aria-haspopup="true" aria-expanded="false"> <span class="iconify" data-icon="mdi:flag"></span> <span class="hidden-lg hidden-md hidden-sm">Traductions de cette page</span><span class="caret"></span> </a> <ul class="dropdown-menu" role="menu"> <li class="dropdown-header hidden-xs hidden-sm"> <span class="iconify" data-icon="mdi:flag"></span> Traductions de cette page </li> <li><div class='li cur'><a href="https://www.irif.fr/rencontres/pps2021/index" class="wikilink1 cur flag" title="Français"><img src="https://www.irif.fr/lib/plugins/translation/flags/fr.gif" alt="fr" height="11" />Français</a></li><li><div class='li'><a href="https://www.irif.fr/en/rencontres/pps2021/index" class="wikilink2 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/rencontres/pps2021/index?do=login&sectok=" title="S'identifier" rel="nofollow" class="menuitem login btn btn-default navbar-btn"><svg xmlns="http://www.w3.org/2000/svg" width="24" height="24" viewBox="0 0 24 24"><path d="M10 17.25V14H3v-4h7V6.75L15.25 12 10 17.25M8 2h9a2 2 0 0 1 2 2v16a2 2 0 0 1-2 2H8a2 2 0 0 1-2-2v-4h2v4h9V4H8v4H6V4a2 2 0 0 1 2-2z"/></svg><span class=""> S'identifier</span></a> </span> </li> </ul> </div> </div> </div> </nav>  </header> <a name="dokuwiki__top" id="dokuwiki__top"></a> <main role="main" class="dw-container pb-5 dokuwiki container-fluid mx-5"> <div id="dokuwiki__pageheader"> <p class="text-right"> </p> <div id="dw__msgarea" class="small"> </div> </div> <div class="row"> <article id="dokuwiki__content" class="col-sm-12 col-md-12 " itemscope itemtype="http://schema.org/Article" itemref="dw__license">  <div class="no-panel" itemprop="articleBody"> <div class="page "> <div class="dw-content-page "><div class="dw-content"><h3 class="sectionedit1 page-header pb-3 mb-4 mt-5" id="journees_pps_2021">Journées PPS 2021</h3> <div class="level3"> <div class="bs-wrap bs-wrap-panel panel panel-default"><div class="panel-heading"><h4 class="panel-title">Preliminary program of the journées PPS 2021</h4></div><div class="panel-body"> <p> After having skipped the 2020 edition due to both the <a href="https://en.wikipedia.org/wiki/List_of_epidemics" class="urlextern" title="https://en.wikipedia.org/wiki/List_of_epidemics" rel="ugc nofollow">sars-cov-2 pandemics</a> and our hopes of organising a physical event after the first wave… here we are! </p> <p> This year the workshop aims at making as many PPS members as possible speak about research topics and problems that they consider worthwhile. </p> <p> You can find below the details of the talks. </p> <p> If you have any question, do not hesitate to contact the organisers: <a href="https://www.irif.fr/~gio/index.xhtml" class="urlextern" title="https://www.irif.fr/~gio/index.xhtml" rel="ugc nofollow">G. Bernardi</a>, <a href="https://www.irif.fr/~faggian/" class="urlextern" title="https://www.irif.fr/~faggian/" rel="ugc nofollow">C. Faggian</a>, <a href="http://pauillac.inria.fr/~herbelin/" class="urlextern" title="http://pauillac.inria.fr/~herbelin/" rel="ugc nofollow">H. Herbelin</a>, <a href="https://www.irif.fr/~saurin/" class="urlextern" title="https://www.irif.fr/~saurin/" rel="ugc nofollow">A. Saurin</a> </p> <p> <strong>On-line rooms</strong> </p> <p> Relax room: <a href="https://gather.town/app/sPyXHQeTooLDzEO5/pps" class="urlextern" title="https://gather.town/app/sPyXHQeTooLDzEO5/pps" rel="ugc nofollow">https://gather.town/app/sPyXHQeTooLDzEO5/pps</a> </p> <p> Talk room for March 22nd (any password works): <a href="https://galene.org:8443/group/seminaire-pps" class="urlextern" title="https://galene.org:8443/group/seminaire-pps" rel="ugc nofollow">https://galene.org:8443/group/seminaire-pps</a> </p> <p> Talk room for the other days: <a href="https://bbb-front.math.univ-paris-diderot.fr/recherche/hug-tje-nwj-dtk" class="urlextern" title="https://bbb-front.math.univ-paris-diderot.fr/recherche/hug-tje-nwj-dtk" rel="ugc nofollow">https://bbb-front.math.univ-paris-diderot.fr/recherche/hug-tje-nwj-dtk</a> </p> <p> Seminar room for the other days: <a href="https://galene.org:8443/group/seminaire-pps" class="urlextern" title="https://galene.org:8443/group/seminaire-pps" rel="ugc nofollow">https://galene.org:8443/group/seminaire-pps</a> </p> </div></div><div class="bs-wrap bs-wrap-panel panel panel-default"><div class="panel-heading"><h4 class="panel-title">Monday 22 March · On-line</h4></div><div class="panel-body"> <p> <strong> 13h45 </strong> <strong>On-line welcome / gathering in the <a href="https://gather.town/app/sPyXHQeTooLDzEO5/pps" class="urlextern" title="https://gather.town/app/sPyXHQeTooLDzEO5/pps" rel="ugc nofollow">relax room</a> </strong> </p> <p> <strong> 14h00 </strong> · <a href="https://www.irif.fr/~jch/" class="urlextern" title="https://www.irif.fr/~jch/" rel="ugc nofollow">J. Chroboczek</a> · Galène, un serveur de vidéoconférence libre </p> <p> <strong> 14h20 </strong> · <a href="https://hugo.feree.fr" class="urlextern" title="https://hugo.feree.fr" rel="ugc nofollow">H. Férée</a> · Implicit Complexity for Higher-Order Functions </p> <p> <strong> 14h40 </strong> · <a href="https://www.irif.fr/~bdelcroix/" class="urlextern" title="https://www.irif.fr/~bdelcroix/" rel="ugc nofollow">B. Delcroix</a> · Posets d'espèces / Species posets </p> <p> <em>15h00 — Coffee break in the <a href="https://gather.town/app/sPyXHQeTooLDzEO5/pps" class="urlextern" title="https://gather.town/app/sPyXHQeTooLDzEO5/pps" rel="ugc nofollow">relax room</a> </em> </p> <p> <strong> 15h10 </strong> · <a href="https://www.irif.fr/~saurin/" class="urlextern" title="https://www.irif.fr/~saurin/" rel="ugc nofollow">A. Saurin</a> · Sur la Séquentialisation et la Construction de Réseaux de Preuves / On Proof-Net Search & Sequentialization </p> <p> <strong> 15h30 </strong> · <a href="https://www.irif.fr/~michele/" class="urlextern" title="https://www.irif.fr/~michele/" rel="ugc nofollow">M. Pagani</a> · Automatic Differentiation in PCF </p> <p> <strong> 15h50 </strong> · <a href="https://www.irif.fr/~gaucher/" class="urlextern" title="https://www.irif.fr/~gaucher/" rel="ugc nofollow">P. Gaucher</a> · Moore flows </p> <p> <em>16h10 — Coffee break in the <a href="https://gather.town/app/sPyXHQeTooLDzEO5/pps" class="urlextern" title="https://gather.town/app/sPyXHQeTooLDzEO5/pps" rel="ugc nofollow">relax room</a> </em> </p> <p> <strong> 16h20 </strong> · <a href="https://www.irif.fr/~buccia/" class="urlextern" title="https://www.irif.fr/~buccia/" rel="ugc nofollow">A. Bucciarelli</a> · An algebraic theory of clones </p> <p> <strong> 16h40 </strong> · <a href="https://music.youtube.com/watch?v=-55HkGzUMRA" class="urlextern" title="https://music.youtube.com/watch?v=-55HkGzUMRA" rel="ugc nofollow">G. Bernardi</a> · Flaky tests, informally </p> <p> <em>17h — End of the first day</em> </p> </div></div><div class="bs-wrap bs-wrap-panel panel panel-default"><div class="panel-heading"><h4 class="panel-title">Tuesday 23 March · On-line</h4></div><div class="panel-body"> <p> <strong> 10h30 </strong> · <strong>Morning seminar</strong> · <a href="https://www.lri.fr/~keller/" class="urlextern" title="https://www.lri.fr/~keller/" rel="ugc nofollow">C. Keller</a> · SMTCoq: safe and efficient automation in Coq </p> <p> <strong> 13h45 </strong> <strong>On-line welcome / gathering in the <a href="https://gather.town/app/sPyXHQeTooLDzEO5/pps" class="urlextern" title="https://gather.town/app/sPyXHQeTooLDzEO5/pps" rel="ugc nofollow">relax room</a> </strong> </p> <p> <strong> 14h00 </strong> · <a href="https://www.irif.fr/users/ade/index" class="urlextern" title="https://www.irif.fr/users/ade/index" rel="ugc nofollow">A. De</a> · Provability of some fixed-point logics </p> <p> <strong> 14h20 </strong> · <a href="https://niols.fr/" class="urlextern" title="https://niols.fr/" rel="ugc nofollow">N. Jeannerod</a> · Verification of Shell Scripts Performing File Hierarchy Transformations (PhD trailer) </p> <p> <strong> 14h40 </strong> · <a href="https://github.com/aspiwack" class="urlextern" title="https://github.com/aspiwack" rel="ugc nofollow">A. Spiwack</a> · Linear types for the masses </p> <p> <em>15h00 — Coffee break in the <a href="https://gather.town/app/sPyXHQeTooLDzEO5/pps" class="urlextern" title="https://gather.town/app/sPyXHQeTooLDzEO5/pps" rel="ugc nofollow">relax room</a> </em> </p> <p> <strong> 15h10 </strong> · <a href="https://www.irif.fr/~jkrivine/homepage/" class="urlextern" title="https://www.irif.fr/~jkrivine/homepage/" rel="ugc nofollow">J. Krivine</a> · Implementing a smart contract for the Ethereum blockchain: a short walk into a Dark Forest </p> <p> <strong> 15h30 </strong> · <a href="https://www.irif.fr/~petrisan/" class="urlextern" title="https://www.irif.fr/~petrisan/" rel="ugc nofollow">D. Petrișan</a> · Combining probabilistic and non-deterministic choice via weak distributive laws </p> <p> <strong> 15h50 </strong> · <a href="https://www.irif.fr/~lpeyrot/" class="urlextern" title="https://www.irif.fr/~lpeyrot/" rel="ugc nofollow"> L. Peyrot </a> · The Spirit of Node Replication </p> <p> <em>16h10 — Coffee break in the <a href="https://gather.town/app/sPyXHQeTooLDzEO5/pps" class="urlextern" title="https://gather.town/app/sPyXHQeTooLDzEO5/pps" rel="ugc nofollow">relax room</a> </em> </p> <p> <strong> 16h20 </strong> · <a href="https://www.irif.fr/~ehrhard/" class="urlextern" title="https://www.irif.fr/~ehrhard/" rel="ugc nofollow">T. Ehrhard </a>· Examples of computations in probabilistic coherence spaces </p> <p> <strong> 16h40 </strong> · <a href="https://www.theozimmermann.net/en/" class="urlextern" title="https://www.theozimmermann.net/en/" rel="ugc nofollow">T. Zimmermann</a> · A model of community organization for the long-term maintenance of an ecosystem's packages </p> <p> <em>17h — End of the second day</em> </p> </div></div><div class="bs-wrap bs-wrap-panel panel panel-default"><div class="panel-heading"><h4 class="panel-title">Monday 29 March · On-line</h4></div><div class="panel-body"> <p> <strong> 13h45 </strong> <strong>On-line welcome / gathering in the <a href="https://gather.town/app/sPyXHQeTooLDzEO5/pps" class="urlextern" title="https://gather.town/app/sPyXHQeTooLDzEO5/pps" rel="ugc nofollow">relax room</a> </strong> </p> <p> <strong> 14h00 </strong> · <a href="https://www.irif.fr/users/nollet/index" class="urlextern" title="https://www.irif.fr/users/nollet/index" rel="ugc nofollow">R. Nollet</a> · Induction and coinduction in Multiplicative Additive Linear Logic </p> <p> <strong> 14h20 </strong> · <a href="https://www.irif.fr/~guetta/" class="urlextern" title="https://www.irif.fr/~guetta/" rel="ugc nofollow">L. Guetta </a> · Looking for models of Homotopy types </p> <p> <strong> 14h40 </strong> · <a href="https://www.irif.fr/~gallego/" class="urlextern" title="https://www.irif.fr/~gallego/" rel="ugc nofollow">E. Gallego</a> · Incremental Type-Checking of Coq Documents </p> <p> <em>15h00 — Coffee break in the <a href="https://gather.town/app/sPyXHQeTooLDzEO5/pps" class="urlextern" title="https://gather.town/app/sPyXHQeTooLDzEO5/pps" rel="ugc nofollow">relax room</a> </em> </p> <p> <strong> 15h10 </strong> · <a href="https://www.irif.fr/~guatto/" class="urlextern" title="https://www.irif.fr/~guatto/" rel="ugc nofollow">A. Guatto</a> · Modalities and Parametric Right Adjoints </p> <p> <strong> 15h30 </strong> · <a href="https://www.irif.fr/en/users/letouzey/index" class="urlextern" title="https://www.irif.fr/en/users/letouzey/index" rel="ugc nofollow">P. Letouzey</a> · Studying Regexps in Coq : Brzozowski, Antimirov and trying to prove the ml-ulex tool </p> <p> <strong> 15h50 </strong> · <a href="http://pauillac.inria.fr/~herbelin/" class="urlextern" title="http://pauillac.inria.fr/~herbelin/" rel="ugc nofollow">H. Herbelin</a> · Effectful proof theory and beyond </p> <p> <em>16h10 — Coffee break in the <a href="https://gather.town/app/sPyXHQeTooLDzEO5/pps" class="urlextern" title="https://gather.town/app/sPyXHQeTooLDzEO5/pps" rel="ugc nofollow">relax room</a></em> </p> <p> <strong> 16h20 </strong> · <a href="http://research.crubille.lautre.net/" class="urlextern" title="http://research.crubille.lautre.net/" rel="ugc nofollow">R. Crubillé</a> · On higher-order cryptography </p> <p> <strong> 16h40 </strong> · C. Gonzalez · Blockchain smartcontracts out of spreadsheets </p> <p> <em>17h — End of the third day</em> </p> <p> <strong> 17h00 </strong> Eva farewell get-together <a href="https://u-paris.zoom.us/j/81215165757?pwd=bVNLWmZURVozT2Y4QVBXcmtsQ3dFdz09" class="urlextern" title="https://u-paris.zoom.us/j/81215165757?pwd=bVNLWmZURVozT2Y4QVBXcmtsQ3dFdz09" rel="ugc nofollow"> in this zoom room </a> </p> </div></div><div class="bs-wrap bs-wrap-panel panel panel-default"><div class="panel-heading"><h4 class="panel-title">Thursday 1 April · On-line</h4></div><div class="panel-body"> <p> <strong> 10h30 </strong> · <strong>Morning seminar</strong> · <a href="https://pages.lip6.fr/Pierre-Evariste.Dagand/" class="urlextern" title="https://pages.lip6.fr/Pierre-Evariste.Dagand/" rel="ugc nofollow">P-E. Dagand</a> · A Programming Model for Transiently-Powered Systems </p> <p> <strong> 13h45 </strong> <strong>On-line welcome / gathering in the <a href="https://gather.town/app/sPyXHQeTooLDzEO5/pps" class="urlextern" title="https://gather.town/app/sPyXHQeTooLDzEO5/pps" rel="ugc nofollow">relax room</a> </strong> </p> <p> <strong> 14h00 </strong> · <a href="http://www.di.unito.it/~curzi/" class="urlextern" title="http://www.di.unito.it/~curzi/" rel="ugc nofollow">G. Curzi</a> · Combining cyclic proofs and implicit complexity </p> <p> <strong> 14h20 </strong> · <a href="https://www.irif.fr/~faggian/" class="urlextern" title="https://www.irif.fr/~faggian/" rel="ugc nofollow">C. Faggian </a> · Asymptotic normalization </p> <p> <strong> 14h40 </strong> · <a href="https://sites.google.com/view/chaitanyals" class="urlextern" title="https://sites.google.com/view/chaitanyals" rel="ugc nofollow">C. Leena Subramaniam</a> · Parametric right adjoint monads, analytic functors, and linear dependent types </p> <p> <em>15h00 — Coffee break in the <a href="https://gather.town/app/sPyXHQeTooLDzEO5/pps" class="urlextern" title="https://gather.town/app/sPyXHQeTooLDzEO5/pps" rel="ugc nofollow">relax room</a> </em> </p> <p> <strong> 15h10 </strong> · AG scientifique </p> <p> <em>17h — <strong>Virtual apéro in the <a href="https://gather.town/app/sPyXHQeTooLDzEO5/pps" class="urlextern" title="https://gather.town/app/sPyXHQeTooLDzEO5/pps" rel="ugc nofollow">relax room</a></strong></em> </p> </div></div><div class="bs-wrap bs-wrap-panel panel panel-default"><div class="panel-heading"><h4 class="panel-title"> J. Chroboczek - Galène, un serveur de vidéoconférence libre</h4></div><div class="panel-body"> <p> Galène (<a href="https://galene.org" class="urlextern" title="https://galene.org" rel="ugc nofollow">https://galene.org</a>) est un serveur de vidéoconférence que j'ai écrit durant le premier confinement français, lorsque la mairie de Paris nous interdisait de sortir de jour de peur qu'on s'amuse mieux qu'eux. </p> <p> Dans cet exposé, je vous raconterai pourquoi j'ai écrit mon propre serveur de vidéoconférence, comment j'ai fait, et comment les gens s'en servent. Je dirai aussi quelques mots sur les avantages des systèmes auto-hébergés (self-hosted), en évitant dans la mesure du possible de vexer les gens (certains de mes meilleurs amis utilisent Gmail). </p> </div></div><div class="bs-wrap bs-wrap-panel panel panel-default"><div class="panel-heading"><h4 class="panel-title"> H. Férée - Implicit Complexity for Higher-Order Functions. </h4></div><div class="panel-body"> <p> Amongst other things, Implicit Complexity aims at helping us better understand complexity classes by obtaining characterisations of various kinds. Besides that, the notion of complexity for higher-order functions is just barely defined, let alone understood. We will here recall the current state of a specific kind of Implicity complexity technique, namely function algebras, and present the motivations and challenges behind its generalisation to functions of order 3 and more. </p> </div></div><div class="bs-wrap bs-wrap-panel panel panel-default"><div class="panel-heading"><h4 class="panel-title"> B. Delcroix-Oger - Posets d'espèces / Species posets</h4></div><div class="panel-body"> <p> Les posets sont des ensembles munis d'un ordre partiel. Les espèces (de structure), introduites par Joyal dans les années 1980, sont des plans de constructions qui permettent de fabriquer des arbres ou des listes à partir de briques interchangeables. Après une présentation des deux protagonistes, je vous ferai visiter différents lieux où ils se cotoient et interagissent. Nous nous arrêterons notamment sur les posets de partition et de Tamari (et associaèdres associés). </p> <p> Posets are Partially Ordered SETS. Species of structure (introduced in the 80s by Joyal) are installation instructions enabling qualified persons to build trees or lists from interchangeable elementary pieces. After a brief introduction of the two lads, we will go on a sightseeing tour of (some of) their meeting places. Two of the main stops will be partition posets and Tamari lattices (and associated associahedron). </p> </div></div><div class="bs-wrap bs-wrap-panel panel panel-default"><div class="panel-heading"><h4 class="panel-title"> A. Saurin - Sur la Séquentialisation et la Construction de Réseaux de Preuves / On Proof-Net Search and Sequentialization</h4></div><div class="panel-body"> <p> Dans cet exposé, je m'intéresserai à la question de la construction de réseaux de preuves en logique linéaire, et j'expliquerai qu'en un certain sens, séquentialisation et construction de réseaux sont deux aspects du même phénomène. </p> <p> Les réseaux de preuves sont des structures logiques où l'ordre des inférences a été (partiellement) oublié: les arbres du calcul des séquents deviennent alors des graphes de structures de preuves. Une conséquence est que la correction logique de l'objet de preuve n'est plus une propriété inductive locale, mais une propriété globale, qui peut être analysée topologiquement: certains graphes sont logiquement corrects (et ils peuvent alors être séquentialisés en une preuve du calcul des séquents) quand d'autres ne le sont pas. On définit ainsi des critères de correction qui caractérisent les graphes corrects (qu'on appelle alors des réseaux de preuves) des autres. </p> <p> Pour étudier la construction de réseaux de preuves, on se placera dans un système logique étendu de structures d'épreuves (ou de para-preuves) en considérant une inférence spéciale permettant de représenter les preuves en construction (ou preuves ouvertes, ou ayant des buts non résolu): il s'agit d'un axiome généralisé similaire au démon de la Ludique. </p> <p> Dans ce cadre élargi, on passera en revue trois critères de correction classiques (Danos-Regnier, Contractibilité et Parsing) dont on mettra en évidence la signification logique: - le premier se réexprime comme un critère interactif: une structure de preuve est correcte si elle passe certains tests; - le second correspond à une séquentialisation distribuée des structures d'épreuves; - le troisième, qui est une spécialisation de la contractibilité, permet d'aborder la question de la construction de réseaux de preuve dont on parlera dans la fin de l'exposé. </p> <p> – </p> <p> In this talk, I will focus on the question of proof-net construction in linear logic and I will explain that sequentialization and proof-net construction can be viewed as two faces of the same coin. </p> <p> Proof-nets are deductive structures in which the order of inference has been (partially) forgotten: sequent calculus derivation trees become graphs of proof structures. As a consequence, logical correctness is not a local, inductive property anymore, but a global one, which may be investigated using topological arguments: some graphs are logically correct (and they can be sequentialized into a sequent proof) while some are not. One defines correctness criteria in order to characterize correct proof structures (aka. proof-nets) from incorrect ones. </p> <p> To study proof-net construction, one will consider an proof system extended to para-proof structures by considering a new inference representing proof-searches (or open proofs, that is with unsolved goals): this inference is a generalized axiom similar to Ludics' daimon. </p> <p> In this extended framework, one shall first review three classical correctness criteria (Danos-Regnier, Contractibility and Parsing) in order to unveil their logical significance: - the first one is an interactive criterion: a para-proof structure is correct if it passes some tests; - the second one corresponds to a form of distributed sequentialization of para-proofs; - the third one, which is a specialization of contractibility, will guide us to the issue of proof-net construction that we shall discuss in the last part of the talk. </p> </div></div><div class="bs-wrap bs-wrap-panel panel panel-default"><div class="panel-heading"><h4 class="panel-title"> M. Pagani - Automatic Differentiation in PCF</h4></div><div class="panel-body"> <p> We study the correctness of automatic differentiation (AD) in the context of a higher-order, Turing-complete language (PCF with real numbers), both in forward and reverse mode. Our main result is that, under mild hypotheses on the primitive functions included in the language, AD is almost everywhere correct, that is, it computes the derivative or gradient of the program under consideration except for a set of Lebesgue measure zero. Stated otherwise, there are inputs on which AD is incorrect, but the probability of randomly choosing one such input is zero. Our result is in fact more precise, in that the set of failure points admits a more explicit description: for example, in case the primitive functions are just constants, addition and multiplication, the set of points where AD fails is contained in a countable union of zero sets of (non-null) polynomials. </p> </div></div><div class="bs-wrap bs-wrap-panel panel panel-default"><div class="panel-heading"><h4 class="panel-title"> P. Gaucher - Moore flows</h4></div><div class="panel-body"> <p> I managed to prove that the q-model structures of multipointed d-spaces (a variant of Grandis' d-spaces) and of flows (a.k.a small semicategories enriched over topological spaces) are Quillen equivalent. The obvious functor from multipointed d-spaces to flows is neither a left nor a right adjoint so it was not a possible candidate, even if its left derived functor already induces an equivalence of categories between the homotopy categories. I have to introduce an intermediate category, the Moore flows, and I can then find a zig-zag of Quillen equivalences between multipointed d-spaces and flows. The idea of introducing Moore flows seems to be a priori absurd since it consists of adding length to morphisms. This well-known method in algebraic topology, introduced by Moore, is a workaround to the fact that the composition of continuous paths is not strictly associative. It becomes strictly associative by considering continuous paths with length. But the composition of morphisms in flows is already strictly associative… In this talk, I will describe the zig-zag of Quillen equivalences. </p> </div></div><div class="bs-wrap bs-wrap-panel panel panel-default"><div class="panel-heading"><h4 class="panel-title"> A. Bucciarelli - An algebraic theory of clones</h4></div><div class="panel-body"> <p> I will present joint work with Antonino Salibra dealing with the notion of “clone of operations”, originated in universal algebra and largely used (without the name) in computer science. Before sketching our algebraic axiomatisation of clones, I will provide an overview of some of these applications. </p> </div></div><div class="bs-wrap bs-wrap-panel panel panel-default"><div class="panel-heading"><h4 class="panel-title"> G. Bernardi - Flaky tests, informally </h4></div><div class="panel-body"> <p> A test that can pass and fail in different runs of the same software is called flaky. Not surprisingly, flaky these are a major industrial issue in software testing. </p> <p> In this talk I we first give overview flaky tests and their impact, and then we sketch the formal methods we propose to tackle the problem in a provably sound manner. </p> </div></div><div class="bs-wrap bs-wrap-panel panel panel-default"><div class="panel-heading"><h4 class="panel-title">Chantal Keller - SMTCoq: safe and efficient automation in Coq</h4></div><div class="panel-body"> <p> The subject of the SMTCoq project is to significantly enhance automation in the Coq proof assistant. At the heart of SMTCoq is a Coq plugin that offers a way to use automatic provers with the same degree of trust as Coq itself. On top of it, we define a framework to progressively encode Coq's logic into first-order logic, through modular and fine-grained logical transformations that can be composed. Our objective is to obtain automatic while expressive tactics for Coq. </p> <p> In this talk, I will concisely introduce the communication between Coq and external provers, before presenting the new framework of logical transformations. I will report on work in progress of examples of transformations in this framework. </p> <p> This is joint work with Valentin Blot, Louise Dubois de Prisque and Pierre Vial. </p> </div></div><div class="bs-wrap bs-wrap-panel panel panel-default"><div class="panel-heading"><h4 class="panel-title">A. De - Provability of some fixed-point logics</h4></div><div class="panel-body"> <p> In this short talk, I will give a high level introduction to the non-wellfounded proof theory of mu-calculus and discuss some questions on the provability of a given sequent. Structural rules are crucial players here. In order, to fully understand their role, we examine the same problems in the linear setting. This is an ongoing work with Alexis Saurin and Anupam Das. </p> </div></div><div class="bs-wrap bs-wrap-panel panel panel-default"><div class="panel-heading"><h4 class="panel-title">N. Jeannerod - Verification of Shell Scripts Performing File Hierarchy Transformations (PhD trailer)</h4></div><div class="panel-body"> <p> In this talk, I will present a trailer of my Ph.D. defence, “Verification of Shell Scripts Performing File Hierarchy Transformations”. I will present the problem we are trying to solve (the quality assurance of Debian software packages) and an overview of how we solve it, as well as a few results. </p> </div></div><div class="bs-wrap bs-wrap-panel panel panel-default"><div class="panel-heading"><h4 class="panel-title"> A. Spiwack - Linear types for the masses</h4></div><div class="panel-body"> <p> I’ve been working, in the past few years, at extending a production-grade compiler (namely GHC, the main Haskell compiler) with linear types. This has the potential of letting linear-logic-style type systems touch a wider public. I’ll be speaking about my experience, and will discuss the newest results on making linear typing easier to use: namely linear constraints, by which we extend Haskell’s type class mechanism to linear logic. </p> </div></div><div class="bs-wrap bs-wrap-panel panel panel-default"><div class="panel-heading"><h4 class="panel-title"> J. Krivine - Implementing a smart contract for the Ethereum blockchain: a short walk into a Dark Forest</h4></div><div class="panel-body"> <p> Implementing smart contract is rather straightforward, but anticipating how it will behave once deployed on a blockchain requires novel ways (at least for me) of thinking about reactive systems. I will discuss the issue of « trusting the code » , « reentrancy », and « slippage ». </p> </div></div><div class="bs-wrap bs-wrap-panel panel panel-default"><div class="panel-heading"><h4 class="panel-title"> D. Petrișan - Combining probabilistic and non-deterministic choice via weak distributive laws</h4></div><div class="panel-body"> <p> It is a well known result that there is no distributive law between the powerset monad and the finite distribution monad. In this talk, I will briefly present a weak distributive law between these monads and a canonical way of composing them. Then I discuss ongoing extensions of this work to a continuous setting. This is joint work with Alexandre Goy. </p> </div></div><div class="bs-wrap bs-wrap-panel panel panel-default"><div class="panel-heading"><h4 class="panel-title"> L. Peyrot - The Spirit of Node Replication </h4></div><div class="panel-body"> <p> Abstract: We define and study a term calculus implementing higher-order node replication. It is used to specify two different (weak) evaluation strategies: call-by-name and fully lazy call-by-need, that are shown to be observationally equivalent by using type theoretical technical tools. </p> </div></div><div class="bs-wrap bs-wrap-panel panel panel-default"><div class="panel-heading"><h4 class="panel-title"> T. Ehrhard - Quelques exemples d'interprétation de programmes dans les espaces cohérents probabilistes</h4></div><div class="panel-body"> <p> Sans entrer dans les définitions techniques, je montrerai quelques interprétations de programmes fonctionnels comme fonctions analytiques entre espaces cohérents probabilistes et je ferai quelques calculs sur ces interprétations. </p> </div></div><div class="bs-wrap bs-wrap-panel panel panel-default"><div class="panel-heading"><h4 class="panel-title"> T. Zimmermann - A model of community organization for the long-term maintenance of an ecosystem's packages</h4></div><div class="panel-body"> <p> In this talk, I present a work-in-progress qualitative study with Jean-Rémy Falleri (LaBRI) about an emerging model of community organization for package maintenance. I have discovered this type of organizations during my PhD, first in the Elm ecosystem, then in several other package ecosystems. These community organizations create a shared space where key ecosystem packages (that would otherwise risk of being abandoned) can be hosted and members of the ecosystem can collaborate in maintaining them. We are adopting a qualitative methodology called “grounded theory”, which originates from sociology, to study these organizations and figure out their key characteristics. Based on this organization model, I have founded the coq-community organization in 2018, and this is now a key component of the Coq ecosystem, as it has attracted more than 30 maintainers and hosts more than 50 packages. </p> </div></div><div class="bs-wrap bs-wrap-panel panel panel-default"><div class="panel-heading"><h4 class="panel-title"> L. Guetta - Looking for models of Homotopy types</h4></div><div class="panel-body"> <p> <em>Disclaimer : Despite the title, my talk is not about “homotopy type theory”. The meaning “homotopy type” is the one from homotopy theory, which is : “space up to homotopy”.</em> </p> <p> In this talk I will present a current interest of mine which is that of finding models for homotopy types. I will first explain precisely what this means and then mention Grothendieck's homotopy conjecture which states that (his definition of) weak ∞-groupoids model homotopy types. Finally, I will very shortly present the notion of n-fold groupoids and explain how they could provide a model for homotopy n-times. </p> </div></div><div class="bs-wrap bs-wrap-panel panel panel-default"><div class="panel-heading"><h4 class="panel-title"> E. Gallego - Incremental Type-Checking of Coq Documents</h4></div><div class="panel-body"> <p> The interactive proof assistant Coq allows provides a strong foundational basis on top of which complex proofs of mathematical theorems and algorithms have been built. </p> <p> A key feature of such proofs is their large size, thus checking that such proofs are valid requires large amounts of computational power and time. This is in conflict with the needs for their effective development, which is usually done via small, incremental changes. </p> <p> As of today, incremental checking of Coq proofs is done at file-level granularity, either using the `make` build system, or the more recent `dune`, which provides some more advanced features such as global caching of build rules, sandboxing, or hash-based target validation. </p> <p> While file-level granularity can significantly reduce incremental checking time, it is still not enough for large projects, CI, and user interfaces, use cases that for different reasons, do suffer from having to re-check complete files if a modification in the dependency tree does occur. </p> <p> In this talk we will present work on `flèche`: an intra-file incremental type checking engine for Coq. Flèche understand dependencies among the objects of a Coq document, and will only re-check parts that are needed, providing large speedups w.r.t. file-level granularity in several interesting use cases. </p> </div></div><div class="bs-wrap bs-wrap-panel panel panel-default"><div class="panel-heading"><h4 class="panel-title"> A. Guatto - Modalities and Parametric Right Adjoints</h4></div><div class="panel-body"> <p> As a wise man said, modal logics are domain-specific logics: various philosophical, mathematical, or computational situations suggest modal extensions to type theory. Each such extension requires careful integration with the syntactic structure of the language, lest its delicate metatheory should falter. I will present recent work by Gratzer, Cavallo, Kavvos, Birkedal and myself proposing a uniform theory of modal extensions based on the category-theoretical notion of parametric right adjoint. </p> </div></div><div class="bs-wrap bs-wrap-panel panel panel-default"><div class="panel-heading"><h4 class="panel-title"> P. Letouzey - Studying Regexps in Coq : Brzozowski, Antimirov and trying to prove the ml-ulex tool</h4></div><div class="panel-body"> <p> Joint work with Yann Régis-Gianas. </p> <p> I'll present the current state of a Coq formalization done with Yann, where we revisited some of the theory of regular expressions and automata : Brzozowski derivatives and the Brzozowski finiteness theorem, Antimirov partial derivatives, and how to build and justify an automata from all that. Then I'll focus on the ml-ulex tool (an “ocamllex”-like from the SML/NJ community, nicely described in [1]) and I'll describe how we tried proving this ml-ulex engine in Coq. And currently, failed… </p> <p> [1] Regular-expression derivatives re-examined, S. Owens, J. Reppy, A. Turon, JFP 2009 </p> </div></div><div class="bs-wrap bs-wrap-panel panel panel-default"><div class="panel-heading"><h4 class="panel-title"> H. Herbelin - Effectful proof theory and beyond</h4></div><div class="panel-body"> <p> I will give a condensed overview of typical questions I'm interested in: </p> <ul class=" fix-media-list-overlap"> <li class="level1"><div class="li"> using exceptions to compute with Markov's principle </div> </li> <li class="level28"><div class="li"> using lazy evaluation of coinductive streams and control to compute with the axiom of dependent choices (with É. Miquey) </div> </li> <li class="level28"><div class="li"> using memory to nicely compute with the theorem of Tarski completeness </div> </li> <li class="level28"><div class="li"> using Lisp's quote to compute with the axiom of extensional choice (with A. Miquel and F. Castro) </div> </li> <li class="level28"><div class="li"> using parametricity to compute with extensional equality (Cubical Type Theory, with H. Moeneclaey) </div> </li> </ul> <p> I will end with a short description of the objectives of πr²'s submitted followup, Picube </p> <ul class=" fix-media-list-overlap"> <li class="level1"><div class="li"> fundamental structures of logic and of mathematical reasoning </div> </li> <li class="level15"><div class="li"> differential and probabilistic tools for programming, reasoning and learning </div> </li> <li class="level15"><div class="li"> architecture and design of a proof assistant for the working mathematician </div> </li> <li class="level15"><div class="li"> formalisation and linguistics of mathematics </div> </li> <li class="level15"><div class="li"> higher dimensional algebra and synthetic homotopy theory </div> </li> </ul> </div></div><div class="bs-wrap bs-wrap-panel panel panel-default"><div class="panel-heading"><h4 class="panel-title"> R. Crubille - On higher-order cryptography</h4></div><div class="panel-body"> <p> Type-two constructions abound in cryptography: adversaries for encryption and authentication schemes, if active, are modeled as algorithms having access to oracles, i.e. as second-order algorithms. But how about making cryptographic schemes themselves higher-order? This work gives an answer to this question, by first describing why higher-order cryptography is interesting as an object of study, then showing how the concept of probabilistic polynomial time algorithm can be generalized so as to encompass algorithms of order strictly higher than two, and finally proving some positive and negative results about the existence of higher-order cryptographic primitives, namely authentication schemes and pseudorandom functions. (joint work with Boaz Barak & Ugo Dal Lago) </p> </div></div><div class="bs-wrap bs-wrap-panel panel panel-default"><div class="panel-heading"><h4 class="panel-title"> C. Gonzalez - Blockchain smartcontracts out of spreadsheets</h4></div><div class="panel-body"> <p> I will talk about my ongoing work as a PhD candidate at the IRIF and Nomadic Labs. This research focuses on providing a tool to design smartcontracts using spreadsheet software as a user interface. The end goal is to design and implement a certified compiler from spreadsheets to the Michelson smart-contratcs language, relying on the recent of work about static differentiation of lambda-calculus in ESOP'19 by Yann Régis-Gianas and his coauthors. </p> </div></div><div class="bs-wrap bs-wrap-panel panel panel-default"><div class="panel-heading"><h4 class="panel-title"> P-E. Dagand - A Programming Model for Transiently-Powered Systems </h4></div><div class="panel-body"> <p> Transiently-powered systems featuring non-volatile memory as well as external peripherals enable the development of new low-power sensor applications. However, as programmers, we are ill-equipped to reason about systems where power failures are the norm rather than the exception. A first challenge consists in being able to capture all the volatile state of the application –external peripherals included– to ensure progress. A second, more fundamental, challenge consists in specifying how power failures may interact with peripheral operations. In a joint work with Rémi Oudin, Delphine Demange, Gautier Berthou and Tanguy Risset, we have proposed a formal specification of intermittent computing with peripherals, an axiomatic model of interrupt-based checkpointing as well as its proof of correctness, machine-checked in the Coq proof assistant. However, this result assumes that the system is able to maintain a shadow copy of the external devices it interacts with. Perhaps surprisingly, this could be an opportunity to adopt an algebraic treatment of external peripherals. </p> </div></div><div class="bs-wrap bs-wrap-panel panel panel-default"><div class="panel-heading"><h4 class="panel-title"> G. Curzi - Combining cyclic proofs and implicit complexity </h4></div><div class="panel-body"> <p> Cyclic proofs (i.e. non-wellfounded but regular proofs) have received growing interest in the literature, and have been proposed as an alternative setting for studying (co)inductive reasoning. However, little is known about the complexity-theoretical aspects of cyclic proofs, which very often exhibit quite convoluted loop structures. This talk is an attempt to bridge the gap between implicit complexity and cyclic proofs. We study a cyclic proof system based on Hofmann’s SLR (Safe Linear Recursion), and we look for suitable proof-theoretical constraints able to reduce the complexity of loops and to capture some interesting complexity classes, such as ELEMENTARY and PTIME. This is joint work with Anupam Das. </p> </div></div><div class="bs-wrap bs-wrap-panel panel panel-default"><div class="panel-heading"><h4 class="panel-title">C. Faggian - Asymptotic normalization </h4></div><div class="panel-body"> <p> I will give some examples of rewriting where termination is asymptotic, that is, the result appears as a limit, as opposite to reaching a normal form in a finite number of steps. Probabilistic computation is a prime example: limits are here distributions over the possible outputs. However, asymptotic termination occurs in settings as diverse as effectful computation, streams, or infinitary lambda-calculi (where the limits are infinitary normal forms such as Boehm trees). I am interested in proof techniques for studying the operational theory of such systems. </p> </div></div><div class="bs-wrap bs-wrap-panel panel panel-default"><div class="panel-heading"><h4 class="panel-title">C. Leena Subramaniam - Parametric right adjoint monads, analytic functors, and linear dependent types </h4></div><div class="panel-body"> <p> Parametric right adjoint (pra) functors (and analytic functors, that can be understood as higher dimensional pra functors) on presheaf categories are multisorted term signatures “with arities” whose operations consume their input in a “linear” way. They strictly generalise the notion of stable functor (resp. analytic functor) from Set to Set. </p> <p> I will present some ideas on how this could be thought of syntactically using dependent types and “linear” dependently typed term signatures. This is very much a work in progress—here be dragons! </p> </div></div> </div> </div></div><p> <style> .page a.urlextern, .page a.interwiki, .page a.windows, .page a.mail, .page a.media { padding-left: 0 !important; background: none !important; } .page { text-align: justify; } body {font-size: 15px; font-weight: 300; color: #333333; } b,strong {font-weight: 600; color: #333333; } p {margin-bottom:1.3em} h1 {font-size: 2.8em; margin-bottom:1.5em; font-weight: 400; } h2 {font-size: 2.2em; margin-bottom:1.2em; font-weight: 400; } h3 {font-size: 1.9em; margin-bottom:0.9em; font-weight: 400; } h4 {font-size: 1.7em; margin-bottom:0.8em; font-weight: 300; } h5 {font-size: 1.5em; margin-bottom:0.8em; font-weight: 300; } h5 {font-size: 1.4em; margin-bottom:0.8em; font-weight: 300; } </style> </p> </div> </div> <div class="small text-right"> </div> </article> </div> </main> <footer id="dw__footer" class="dw-container py-5 dokuwiki container-fluid">  <div class="dw-container small container-fluid mx-5"> <div class="footer-dw-title"> <div class="media"> <div class="media-left">  <img src="https://www.irif.fr/_media/logo_footer.png" alt="" class="media-object" style="height:10px" /> </div> <div class="media-body"> <div class="row"> <div class="col-sm-2"> <h4 class="media-heading"></h4> <p> </p> </div> <div class="col-sm-10"> </div> </div> </div> </div> </div> <a style="font-size:12px" href="https://www.irif.fr/informations/mentions-legales">Mentions légales</a> <div class="footer-license row"> <hr/> <div id="dw__license" class="col-sm-6"> </div> <div class="col-sm-6"> </div> </div> </div>  </footer> <a href="#dokuwiki__top" class="back-to-top hidden-print btn btn-default" title="Aller au contenu" accesskey="t"> <span class="iconify" data-icon="mdi:chevron-up"></span> </a> <div id="screen__mode"> <span class="visible-xs-block"></span> <span class="visible-sm-block"></span> <span class="visible-md-block"></span> <span class="visible-lg-block"></span> </div> <img src="https://www.irif.fr/lib/exe/taskrunner.php?id=rencontres%3Apps2021%3Aindex&1732983124" width="2" height="1" alt="" /> </div> </body> </html>