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>La syntaxe rencontre la sémantique</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="seminaires,sms,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/seminaires/sms/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/seminaires/sms/index"/> <link rel="alternate" type="text/plain" title="Wiki balise" href="https://www.irif.fr/_export/raw/seminaires/sms/index"/> <link rel="canonical" href="https://www.irif.fr/seminaires/sms/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='seminaires:sms';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":"seminaires:sms:index","namespace":"seminaires:sms","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="seminaires:sms: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 active 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 active"> <a href="https://www.irif.fr/seminaires/sms/index" class="wikilink1" title="seminaires:sms:index" data-wiki-curid="true">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/seminaires/sms/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/seminaires/sms/index" class="wikilink1 flag" title="English"><img src="https://www.irif.fr/lib/plugins/translation/flags/en.gif" alt="en" height="11" />English</a></li> </ul> </li> </ul>  <ul class="nav navbar-nav"> <li> <span class="dw__actions dw-action-icon"> <a href="https://www.irif.fr/seminaires/sms/index?do=login&sectok=" title="S'identifier" rel="nofollow" class="menuitem login btn btn-default navbar-btn"><svg xmlns="http://www.w3.org/2000/svg" width="24" height="24" viewBox="0 0 24 24"><path d="M10 17.25V14H3v-4h7V6.75L15.25 12 10 17.25M8 2h9a2 2 0 0 1 2 2v16a2 2 0 0 1-2 2H8a2 2 0 0 1-2-2v-4h2v4h9V4H8v4H6V4a2 2 0 0 1 2-2z"/></svg><span class=""> S'identifier</span></a> </span> </li> </ul> </div> </div> </div> </nav>  </header> <a name="dokuwiki__top" id="dokuwiki__top"></a> <main role="main" class="dw-container pb-5 dokuwiki container-fluid mx-5"> <div id="dokuwiki__pageheader"> <p class="text-right"> </p> <div id="dw__msgarea" class="small"> </div> </div> <div class="row"> <article id="dokuwiki__content" class="col-sm-12 col-md-12 " itemscope itemtype="http://schema.org/Article" itemref="dw__license">  <div class="no-panel" itemprop="articleBody"> <div class="page "> <div class="dw-content-page "><div class="dw-content"><div class="plugin_include_content plugin_include__seminaires:sms:indexheader" id="plugin_include__seminaires__sms__indexheader"> <div class="datatemplateentry"> <p> <br/> </p> <div class="wrap_right plugin_wrap"> <p> <div class="bs-wrap bs-wrap-well well"> <span class="bs-wrap bs-wrap-button" data-btn-type="primary" data-btn-size="sm" data-btn-disabled="1">Groupe de travail</span> </p> <div class=""> <p> <span class="bs-wrap bs-wrap-label label label-default">Pôle</span> <a href="https://www.irif.fr/seminaires/sms/0_pageid" class="wikilink2" title="seminaires:sms:0_pageid" rel="nofollow" data-wiki-id="seminaires:sms:0_pageid"><a href="https://www.irif.fr/poles/pps/index" class="wikilink1" title="poles:pps:index" data-wiki-id="poles:pps:index">Preuves, programmes et systèmes</a></a><br/> </p> </div><div class=""> <p> <span class="bs-wrap bs-wrap-label label label-default">Équipe thématique</span> <a href="https://www.irif.fr/seminaires/sms/0_pageid" class="wikilink2" title="seminaires:sms:0_pageid" rel="nofollow" data-wiki-id="seminaires:sms:0_pageid"><a href="https://www.irif.fr/equipes/preuves/index" class="wikilink1" title="equipes:preuves:index" data-wiki-id="equipes:preuves:index">Preuves et programmes</a></a><br/> </p> </div> <p> </div> </p> <div style='display:none'><div class="wrap_right plugin_wrap"> <p> <span class="bs-wrap bs-wrap-button" data-btn-type="default"><a href="https://www.irif.fr/admindb/seminaires/" class="urlextern" title="https://www.irif.fr/admindb/seminaires/" rel="ugc nofollow">Gestion des séances</a></span> </p> </div></div></div> <h2 id="la_syntaxe_rencontre_la_semantique" class=" page-header pb-3 mb-4 mt-5">La syntaxe rencontre la sémantique</h2> <div class="level2"> <p> <br/> </p> </div> <h4 id="jour_heure_et_lieu">Jour, heure et lieu</h4> <div class="level4"> <p> Le jeudi à 14h, salle 1007 </p> <p> Le <a href="http://www.irif.fr/_media/ical/sms.ics" class="urlextern" title="http://www.irif.fr/_media/ical/sms.ics" rel="ugc nofollow">calendrier</a> des séances (format iCal). <br/> Pour ajouter le calendrier des séances à votre agenda favori, souscrire au calendrier en indiquant ce lien. </p> <p> <br/> </p> </div> <h4 id="contact_s">Contact(s)</h4> <div class="level4"> <div class=""> <p> <a href="https://www.irif.fr/~kesner" class="urlextern" title="https://www.irif.fr/~kesner" rel="ugc nofollow">Delia Kesner</a><br/> </p> </div> </div> </div> <p> Subscribe to the list gdt-sms@listes.irif.fr to receive announcements concerning this working work. </p> </div> <p> <br/> </p> <h3 class="sectionedit3 page-header pb-3 mb-4 mt-5" id="prochaines_seances">Prochaines séances</h3> <div class="level3"> <p> <a href="https://www.irif.fr/seminaires/sms/index" class="wikilink1" title="seminaires:sms:index" data-wiki-id="seminaires:sms:index">La syntaxe rencontre la sémantique</a><br/> Jeudi 12 décembre 2024, 13 heures 30, Salle 3052<br/> <strong>Pablo Barenbaum</strong> (UNQ, Argentine) <em>Non encore annoncé.</em> <br/> </p> <p> <a href="https://www.irif.fr/seminaires/sms/index" class="wikilink1" title="seminaires:sms:index" data-wiki-id="seminaires:sms:index">La syntaxe rencontre la sémantique</a><br/> Jeudi 16 janvier 2025, 13 heures 30, Salle 3052<br/> <strong>Gaëtan Lopez</strong> (IRIF, UPC) <em>A Rewriting Theory for Quantum λ-Calculus</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b31-4309"><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="b31-4309"><div class="bs-wrap bs-wrap-well well well-sm"> Quantum lambda calculus has been studied mainly as an idealized programming language—the evaluation essentially corresponds to a deterministic abstract machine. Very little work has been done to develop a rewriting theory for quantum lambda calculus. Recent advances in the theory of probabilistic rewriting give us a way to tackle this task with tools unavailable a decade ago. Our primary focus is standardization and normalization results. </div> </div> <p> <br/> </p> </div> <h3 class="sectionedit4 page-header pb-3 mb-4 mt-5" id="seances_passees">Séances passées</h3> <div class="level3"> <p> <br/> </p> </div> <h4 id="annee_2024">Année 2024</h4> <div class="level4"> </div> <div class="plugin_include_content plugin_include__seminaires:sms:sms2024" id="plugin_include__seminaires__sms__sms2024"> <div class="level4"> <p> <a href="https://www.irif.fr/seminaires/sms/index" class="wikilink1" title="seminaires:sms:index" data-wiki-id="seminaires:sms:index">La syntaxe rencontre la sémantique</a><br/> Jeudi 14 novembre 2024, 14 heures 30, Salle 3052<br/> <strong>Adrienne Lancelot</strong> (LIX et IRIF) <em>Interaction Equivalence</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b31-4310"><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="b31-4310"><div class="bs-wrap bs-wrap-well well well-sm"> Contextual equivalence is the de facto standard notion of program equivalence. A key theorem is that contextual equivalence is an equational theory. Making contextual equivalence more intensional, for example taking into account the time cost of the computation, seems a natural refinement. Such a change, however, does not induce an equational theory, for an apparently essential reason: cost is not invariant under reduction. <p> In the paradigmatic case of the untyped λ-calculus, we introduce interaction equivalence. Inspired by game semantics, we observe the number of interaction steps between terms and contexts but—crucially—ignore their own internal steps. We prove that interaction equivalence is an equational theory and we characterize it as B, the well-known theory induced by Böhm tree equality. Ours is the first observational characterization of B obtained without enriching the discriminating power of contexts with extra features such as non-determinism. To prove our results, we develop interaction-based refinements of the Böhm-out technique and of intersection types. </div> </p> </div> <p> <a href="https://www.irif.fr/seminaires/sms/index" class="wikilink1" title="seminaires:sms:index" data-wiki-id="seminaires:sms:index">La syntaxe rencontre la sémantique</a><br/> Jeudi 10 octobre 2024, 14 heures, Salle 3052<br/> <strong>Jorge A. Pérez</strong> (University of Groningen) <em>The Expressiveness of Session Types</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b31-4311"><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="b31-4311"><div class="bs-wrap bs-wrap-well well well-sm"> Session types are a typed approach to ensure the communication correctness of message-passing programs. They have been extensively studied from a theoretical standpoint, and have been also incorporated into diverse programming languages and models. <p> Perhaps surprisingly, there is no single, canonical session type system, but many. It is fair to say that expressiveness has been key to the success and impact of session types: enhancing the expressivity of typed processes and/or the properties enforced by typing is often a strong motivation for developing new typed frameworks. </p> <p> In this rich and diverse context, rigorously contrasting different variants of session types from an expressiveness perspective is a fascinating and non-trivial challenge. In this talk I introduce session types briefly and overview some recent works related to their expressiveness; they cover various angles, including “propositions-as-sessions”, i.e., the Curry-Howard correspondence between session types and linear logic. </div> </p> </div> <p> <a href="https://www.irif.fr/seminaires/sms/index" class="wikilink1" title="seminaires:sms:index" data-wiki-id="seminaires:sms:index">La syntaxe rencontre la sémantique</a><br/> Jeudi 20 juin 2024, 14 heures, Salle 3052<br/> <strong>Victor Arrial</strong> (IRIF, Universite Paris Cite) <em>The Benefits of Diligence</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b31-4312"><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="b31-4312"><div class="bs-wrap bs-wrap-well well well-sm"> In this talk, we will discuss the strength of embedding Call-by-Name (dCBN) and Call-by-Value (dCBV) into a unifying framework called the Bang Calculus (dBANG). These embeddings enable establishing (static and dynamic) properties of dCBN and dCBV through their respective counterparts in dBANG. While some specific static properties have been already successfully studied in the literature, the dynamic ones are more challenging and have been left unexplored. We accomplish that by using a standard embedding for the (easy) dCBN case, while a novel one must be introduced for the (difficult) dCBV case. Moreover, a key point of our approach is the identification of dBANG diligent reduction sequences, which eases the preservation of dynamic properties from dBANG to dCBN/dCBV. We illustrate our methodology through two concrete applications: confluence/factorization for both dCBN and dCBV are respectively derived from confluence/factorization for dBANG. </div> </div> <p> <a href="https://www.irif.fr/seminaires/sms/index" class="wikilink1" title="seminaires:sms:index" data-wiki-id="seminaires:sms:index">La syntaxe rencontre la sémantique</a><br/> Jeudi 6 juin 2024, 14 heures, Salle 3052<br/> <strong>Adrienne Lancelot</strong> (LIX Polytechnique and IRIF UPC) <em>Mirroring Call-by-Need, or Values Acting Silly</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b31-4313"><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="b31-4313"><div class="bs-wrap bs-wrap-well well well-sm"> Call-by-need evaluation for the lambda-calculus can be seen as merging the best of call-by-name and call-by-value, namely the wise erasing behaviour of the former and the wise duplicating behaviour of the latter. To better understand how duplication and erasure can be combined, we design a degenerated calculus, dubbed call-by-silly, that is symmetric to call-by-need in that it merges the worst of call-by-name and call-by-value, namely silly duplications by-name and silly erasures by-value. <p> We validate the design of the call-by-silly calculus via rewriting properties and multi types. In particular, we mirror the main theorem about call-by-need – that is, its operational equivalence with call-by-name – showing that call-by-silly and call-by-value induce the same contextual equivalence. This fact shows the blindness with respect to efficiency of call-by-value contextual equivalence. We also define a call-by-silly strategy and measure its length via tight multi types. Lastly, we prove that the call-by-silly strategy computes evaluation sequences of maximal length in the calculus. </div> </p> </div> <p> <a href="https://www.irif.fr/seminaires/sms/index" class="wikilink1" title="seminaires:sms:index" data-wiki-id="seminaires:sms:index">La syntaxe rencontre la sémantique</a><br/> Jeudi 2 mai 2024, 14 heures, Salle 3071<br/> <strong>Mariana Milicich</strong> (IRIF, Universite Paris Cite) <em>Hybrid Intersection Types for PCF</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b31-4314"><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="b31-4314"><div class="bs-wrap bs-wrap-well well well-sm"> I will present a type system based on non-idempotent intersection types for PCFh, a variant of PCF. Evaluation in PCFh is hybrid: call-by-name (CBN) and call-by-value (CBV) behaviours cohabit together. Specifically, function application follows CBV semantics, while recursion has a CBN flavour. This hybrid nature is reflected in the type system, which turns out to be sound and complete with respect to PCFh evaluation. This means not only that typability implies normalisation, but also that the converse holds. Moreover, the type system is quantitative, since the size of typing derivations provides upper bounds for the length of normalisation sequences. By refining this type system, we obtain a tight type system, which offers exact information regarding the length of normalisation sequences. </div> </div> <p> <a href="https://www.irif.fr/seminaires/sms/index" class="wikilink1" title="seminaires:sms:index" data-wiki-id="seminaires:sms:index">La syntaxe rencontre la sémantique</a><br/> Jeudi 28 mars 2024, 14 heures, Salle 3052<br/> <strong>Noam Zeilberger</strong> (LIX, Polytechnique) <em>An introduction to type refinement systems</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b31-4315"><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="b31-4315"><div class="bs-wrap bs-wrap-well well well-sm"> I will give an introduction to type refinement systems in the style of Frank Pfenning et al., discuss the phenomenon of how refinement typing makes some aspects of evaluation order visible in the type system, and give some general indications of how type refinement may be understood from a categorical perspective. For background reading, you can see my notes from OPLSS 2016 on “Principles of type refinement” (<a href="https://noamz.org/oplss16/refinements-notes.pdf" class="urlextern" title="https://noamz.org/oplss16/refinements-notes.pdf" rel="ugc nofollow">https://noamz.org/oplss16/refinements-notes.pdf</a>). </div> </div> <p> <a href="https://www.irif.fr/seminaires/sms/index" class="wikilink1" title="seminaires:sms:index" data-wiki-id="seminaires:sms:index">La syntaxe rencontre la sémantique</a><br/> Jeudi 15 février 2024, 14 heures, Salle 3052<br/> <strong>Hector Suzanne</strong> (LIP6) <em>Une machine abstraite Call-By-Push-Value pour l'analyse de ressource</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b31-4316"><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="b31-4316"><div class="bs-wrap bs-wrap-well well well-sm"> Dans le but de factoriser et étendre les techniques d'Analyses Amorties de Ressource Automatisées, nous introduisons une machine abstraite comme représentation intermédiaire pour étendre les possibilités d'analyses aux langages linéaires et à sémantiques Call-By-Push-Value (CBPV), qui intègre à la fois l'appel par valeur et l'appel par nom. <p> La machine est une extension de la machine ILL_rho^eta de Curien et al.[1] avec des points fixes et une dépendance des types sur des paramètres de structures (taille, longueur, coût) qui sont contraints par une formule du premier ordre. Une phase de réécriture systématique, de et vers la machine, enrichit les programmes et définitions d'ADT avec des annotations de paramètres, de passage d'état et des primitives de coût. Elle implémente AARA comme un effet qui produit à la compilation une approximation sûre des manipulations de ressources à l'exécution. </p> <p> Nous présentons l'exemple d'un miniML en appel par valeur des avec blocs monadiques et transformeurs de monades pour l'état mutable et les exceptions locales. L'analyse AARA demeure inchangée grâce aux implémentations canoniques des primitives monadiques dans CBPV. Une procédure de typage basée sur HM(X) a été implémentée et génère une contrainte globale sur les paramètres du programme entiers. Dans le cas classique où les coûts sont représentés par les polynômes en plusieurs variables, une procédure d'élimination des quantificateurs permet de se ramener à la programmation entière pour instancier des bornes explicites via un solveur externe. </p> <p> Cet exposé reprend en grande partie le travail qui a été présenté à la conférence LOPSTR 2023 [2] </p> <p> [1] doi.org/10.1145/2837614.2837652 [2] doi.org/10.1007/978-3-031-45784-5_5 </div> </p> </div> <p> <a href="https://www.irif.fr/seminaires/sms/index" class="wikilink1" title="seminaires:sms:index" data-wiki-id="seminaires:sms:index">La syntaxe rencontre la sémantique</a><br/> Jeudi 25 janvier 2024, 14 heures, Visio<br/> <strong>Davide Catta</strong> (Università degli Studi di Napoli Federico II) <em>Game semantics and a new lambda calculus for the constructive modal logic CK</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b31-4317"><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="b31-4317"><div class="bs-wrap bs-wrap-well well well-sm"> Constructive modal logics are extensions of intuitionistic logic obtained by adding unary operators, called modalities, to the language of intuitionistic logic. These logics have generated increasing interest over the past decades, being investigated from both proof theory and type theory perspectives. <p> In this talk, we investigate the Curry-Howard correspondence for constructive modal logic CK in light of the gap between the proof equivalences enforced by the lambda calculi from the literature and by the recently defined winning strategies for this logic. </p> <p> We present a game semantics for CK and a new lambda-calculus system for this logic, obtained by enriching the calculus from the literature with additional reduction rules. We then provide a typing system in the style of focused proof systems, allowing us to provide a unique proof for each term in normal form. Finally, we use this result to show a one-to-one correspondence between terms in normal form and winning innocent strategies for CK. </p> <p> (Joint work with Matteo Acclavio and Federico Olimpieri). </div> </p> </div> <p> <a href="https://www.irif.fr/seminaires/sms/index" class="wikilink1" title="seminaires:sms:index" data-wiki-id="seminaires:sms:index">La syntaxe rencontre la sémantique</a><br/> Jeudi 18 janvier 2024, 15 heures, Salle 1007<br/> <strong>Jui-Hsuan Wu</strong> (LIX, Polytechnique) <em>Proofs as terms, positively</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b31-4318"><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="b31-4318"><div class="bs-wrap bs-wrap-well well well-sm"> Structural proof theory has been widely used in the study of term structures. In this talk, I will illustrate this tight connection between proofs and terms by presenting the focused proof system LJF as a framework for designing term structures. Since the proof theory of LJF does not pick a canonical polarization for atomic formulas, two different approaches to term representation arise. We will illustrate these two approaches by applying them to the encoding of untyped lambda terms. When atomic formulas are given the negative polarity, LJF proofs yield the usual tree-like representation of untyped lambda terms. When atomic formulas are given the positive polarity, LJF proofs yield a term structure in which sharing is possible via explicit substitution. In the second part of the talk, I will present the positive lambda calculus, a calculus with explicit substitution based on the positive polarization, and show its close relationship with Accattoli and Paolini's value substitution calculus. </div> </div> </div> </div> <div class="level4"> <p> <br/> </p> </div> <h4 id="annee_2023">Année 2023</h4> <div class="level4"> </div> <div class="plugin_include_content plugin_include__seminaires:sms:sms2023" id="plugin_include__seminaires__sms__sms2023"> <div class="level4"> <p> <a href="https://www.irif.fr/seminaires/sms/index" class="wikilink1" title="seminaires:sms:index" data-wiki-id="seminaires:sms:index">La syntaxe rencontre la sémantique</a><br/> Jeudi 21 décembre 2023, 14 heures, Salle 3052<br/> <strong>Gabriel Scherer</strong> (INRIA) <em>Constructor unboxing</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b31-4319"><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="b31-4319"><div class="bs-wrap bs-wrap-well well well-sm"> In this work I will present a new feature proposed for the OCaml programming language, “constructor unboxing”, first suggested by Jeremy Yallop in March 2020. It enables a more efficient representation of certain sum types, but requires a static analysis to forbid certain unboxing requests that would be unsound. <p> To define this static analysis, one has to solve a problem of normalization of first-order definitions in presence of recursion. In the talk I hope to explain my current understanding of this halting problem, and present an algorithm to compute normal forms and reject (in finite time) non-normalizable definitions. </div> </p> </div> <p> <a href="https://www.irif.fr/seminaires/sms/index" class="wikilink1" title="seminaires:sms:index" data-wiki-id="seminaires:sms:index">La syntaxe rencontre la sémantique</a><br/> Jeudi 7 décembre 2023, 14 heures, Salle 3052<br/> <strong>Pablo Barenbaum</strong> (Universidad Buenos Aires) <em>Sharing in linear logic and call-by-need</em> <br/> </p> <p> <a href="https://www.irif.fr/seminaires/sms/index" class="wikilink1" title="seminaires:sms:index" data-wiki-id="seminaires:sms:index">La syntaxe rencontre la sémantique</a><br/> Jeudi 26 octobre 2023, 14 heures, salle 1007<br/> <strong>Giuseppe Castagna</strong> (IRIF, CNRS and Univ. Paris Cite) <em>A type system for Elixir</em> <br/> </p> <p> <a href="https://www.irif.fr/seminaires/sms/index" class="wikilink1" title="seminaires:sms:index" data-wiki-id="seminaires:sms:index">La syntaxe rencontre la sémantique</a><br/> Jeudi 12 octobre 2023, 14 heures, salle 3052<br/> <strong>Mariana Milicich</strong> (Université Paris Cité, CNRS, IRIF) <em>Useful Evaluation, Inductively and Quantitatively</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b31-4320"><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="b31-4320"><div class="bs-wrap bs-wrap-well well well-sm"> Is λ-calculus a reasonable machine according to Van Emde Boas' Invariance Thesis? By defining the useful evaluation strategy, B. Accattoli and U. Dal Lago were able to answer positively to this question. However, their characterization doesn't facilitate the use of inductive arguments to reason about it. And, up to this date, there are no quantitative models to capture its time complexity. <p> In this talk I'll discuss the first inductive characterization of the useful evaluation for open call-by-value. We achieve this by parameterizing the evaluation relation with respect to the information provided by the context in which the computation takes place. First we prove some properties of our notion of useful calculus. Then, we give a quantitative model for the useful strategy, using a non-idempotent intersection type system with tight rules. Therefore, typing a term t gives exact information about how many steps does the computation requires to compute the normal form of t. </div> </p> </div> <p> <a href="https://www.irif.fr/seminaires/sms/index" class="wikilink1" title="seminaires:sms:index" data-wiki-id="seminaires:sms:index">La syntaxe rencontre la sémantique</a><br/> Jeudi 28 septembre 2023, 14 heures, Salle 3052<br/> <strong>Beniamino Accattoli</strong> (INRIA Saclay) <em>Closure Conversion and Abstract Machines</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b31-4321"><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="b31-4321"><div class="bs-wrap bs-wrap-well well well-sm"> Closure conversion is a program transformation at work in compilers for functional languages to turn inner functions into global ones, by building 'closures' pairing the transformed functions with the 'environment' of their free variables. Abstract machines rely on similar and yet different concepts of 'closures' and 'environments'. <p> In this talk, we analyze the relationship between the two approaches. We adopt a very simple lambda-calculus with tuples as source language and study abstract machines for both the source language and the target of closure conversion. </p> <p> We overview three contributions. Firstly, a new simple proof technique for the correctness of closure conversion, inspired by abstract machines. Secondly, we show how the closure invariants of the target language allow us to design a new way of handling environments in abstract machines, not suffering the shortcomings of other styles. Thirdly, we analyze the machines from the point of view of sharing and time complexity, dissecting how different aspects of closure conversion impact on the cost of the execution. </div> </p> </div> <p> <a href="https://www.irif.fr/seminaires/sms/index" class="wikilink1" title="seminaires:sms:index" data-wiki-id="seminaires:sms:index">La syntaxe rencontre la sémantique</a><br/> Jeudi 22 juin 2023, 14 heures, salle 146 (Olympe de Gouges)<br/> <strong>Miguel Ramos</strong> (Univ. Porto) <em>Quantitative CBV Global Memory</em> <br/> </p> <p> <a href="https://www.irif.fr/seminaires/sms/index" class="wikilink1" title="seminaires:sms:index" data-wiki-id="seminaires:sms:index">La syntaxe rencontre la sémantique</a><br/> Jeudi 1 juin 2023, 14 heures, salle 146 (Olympe de Gouges)<br/> <strong>Gabriele Vanoni</strong> (Univ. Bologna) <em>Higher-Order and Non-Linear Bayesian Networks</em> <br/> </p> <p> <a href="https://www.irif.fr/seminaires/sms/index" class="wikilink1" title="seminaires:sms:index" data-wiki-id="seminaires:sms:index">La syntaxe rencontre la sémantique</a><br/> Mercredi 24 mai 2023, 14 heures, salle 147 (Olympe de Gouges)<br/> <strong>Jose Espirito Santo</strong> (Univ. Minho (Portugal)) <em>The logical essence of compiling with continuations</em> <br/> </p> <p> <a href="https://www.irif.fr/seminaires/sms/index" class="wikilink1" title="seminaires:sms:index" data-wiki-id="seminaires:sms:index">La syntaxe rencontre la sémantique</a><br/> Jeudi 20 avril 2023, 13 heures 30, salle 147 (Olympe de Gouges)<br/> <strong>Hugo Herbelin</strong> (IRIF, INRIA, Univ. Paris Cite) <em>Under syntax and semantics, the logic</em> <br/> </p> <p> <a href="https://www.irif.fr/seminaires/sms/index" class="wikilink1" title="seminaires:sms:index" data-wiki-id="seminaires:sms:index">La syntaxe rencontre la sémantique</a><br/> Jeudi 30 mars 2023, 13 heures 30, salle 4052<br/> <strong>Nino Salibra</strong> (Universita' Ca'Foscari Venezia) <em>A completeness theorem for the infinitary lambda calculus</em> <br/> </p> <p> <a href="https://www.irif.fr/seminaires/sms/index" class="wikilink1" title="seminaires:sms:index" data-wiki-id="seminaires:sms:index">La syntaxe rencontre la sémantique</a><br/> Mardi 28 mars 2023, 13 heures 30, salle 3052<br/> <strong>Fabio Massaioli (Scuola Normale Di Pisa)</strong> (Scuola Normale di Pisa) <em>A non-trivial proof-semantics for classical sequent calculus (LK)</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b31-4322"><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="b31-4322"><div class="bs-wrap bs-wrap-well well well-sm"> Cut-reduction procedures for classical sequent calculus are notoriously non-deterministic and non-confluent, both in the original formulation by Gentzen and in later reformulations. It is natural to ask whether those instances of non-confluence are superficial in nature, i.e. whether syntactically distinct normal forms of the same derivation are in fact correlated in a non-trivial way, as is the case in the intuitionistic and linear versions of sequent calculus. A famous counter-example by Lafont purports to show that the answer is negative, that is, every interpretation of derivations in LK that is invariant under classical cut-elimination must be a trivial one that identifies at least all proofs of the same sequent. A long-standing open question has then been whether it could be possible to work around Lafont's example by natural and non-trivial adjustments of the calculus and/or of cut-reduction steps, without resorting to symmetry-breaking techniques like polarization or embeddings into intuitionistic or linear logic. <p> Working within the propositional fragment of the context-sharing formulation of LK — where parallel logical rules permute freely — we show that the graph constructed by tracing the history of atomic formula occurrences through axiom and cut rules is invariant under arbitrary rule permutations in cut-free proofs, thus providing a canonical representation of normal-form proofs. </p> <p> We then introduce a refinement of the notion of axiom-induced graph that allows extending the invariance result to proofs with cuts, although at the cost of a strong assumption on the shape of derivations. Because cut-reduction in this formulation of LK can be implemented entirely by logical rule permutations plus a pair of local rewriting steps that preserve the refined axiom graphs, the result yields a non-trivial invariant of cut-reduction. </div> </p> </div> <p> <a href="https://www.irif.fr/seminaires/sms/index" class="wikilink1" title="seminaires:sms:index" data-wiki-id="seminaires:sms:index">La syntaxe rencontre la sémantique</a><br/> Jeudi 9 mars 2023, 14 heures, salle 1007<br/> <strong>Daniele Pautasso</strong> (Univ. Torino) <em>A quantitative version of simple types</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b31-4323"><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="b31-4323"><div class="bs-wrap bs-wrap-well well well-sm"> Our work introduces a quantitative version of the simple type assignment system, starting from a suitable restriction of non-idempotent intersection types. The key idea is to restrict multiset formation to uniform types, two types being uniform if they differ only in the cardinality of the multisets occurring in it. The resulting system has the same typability power as the simple type assignment system; thus, assigning types to terms supplies the very same qualitative information given by simple types, but at the same time provides some interesting quantitative information. It is well known that typability for simple types is equivalent to unification; we prove a similar result for the newly introduced system. More precisely, we show that typability is equivalent to a unification problem which is a non-trivial extension of the classical one: in addition to unification rules, our typing algorithm makes use of an operation that increases the cardinality of multisets whenever needed. </div> </div> <p> <a href="https://www.irif.fr/seminaires/sms/index" class="wikilink1" title="seminaires:sms:index" data-wiki-id="seminaires:sms:index">La syntaxe rencontre la sémantique</a><br/> Jeudi 2 mars 2023, 14 heures, salle 1007<br/> <strong>Riccardo Treglia</strong> <em>Intersecting effects: two orthogonal approaches</em> <br/> </p> <p> <a href="https://www.irif.fr/seminaires/sms/index" class="wikilink1" title="seminaires:sms:index" data-wiki-id="seminaires:sms:index">La syntaxe rencontre la sémantique</a><br/> Jeudi 9 février 2023, 14 heures, salle 1007<br/> <strong>Giovanni Bernardi</strong> <em>Breaking circles</em> <br/> </p> <p> <a href="https://www.irif.fr/seminaires/sms/index" class="wikilink1" title="seminaires:sms:index" data-wiki-id="seminaires:sms:index">La syntaxe rencontre la sémantique</a><br/> Jeudi 26 janvier 2023, 14 heures, salle 1007<br/> <strong>Sandra Alves</strong> <em>Quantitative Weak Linearisation</em> <br/> </p> <p> <a href="https://www.irif.fr/seminaires/sms/index" class="wikilink1" title="seminaires:sms:index" data-wiki-id="seminaires:sms:index">La syntaxe rencontre la sémantique</a><br/> Jeudi 12 janvier 2023, 14 heures, salle 1007<br/> <strong>Les Doctorants Du Groupe De Travail</strong> (Universite Paris Cite) <em>Présentation des doctorants du groupe et de leur thématique de recherche</em> <br/> </p> </div> </div> <div class="level4"> <p> <br/> </p> </div> <h4 id="annee_2022">Année 2022</h4> <div class="level4"> </div> <div class="plugin_include_content plugin_include__seminaires:sms:sms2022" id="plugin_include__seminaires__sms__sms2022"> <div class="level4"> <p> <a href="https://www.irif.fr/seminaires/sms/index" class="wikilink1" title="seminaires:sms:index" data-wiki-id="seminaires:sms:index">La syntaxe rencontre la sémantique</a><br/> Jeudi 15 décembre 2022, 14 heures, salle 1007<br/> <strong>Victor Arrial</strong> <em>Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework</em> <br/> </p> <p> <a href="https://www.irif.fr/seminaires/sms/index" class="wikilink1" title="seminaires:sms:index" data-wiki-id="seminaires:sms:index">La syntaxe rencontre la sémantique</a><br/> Jeudi 3 novembre 2022, 14 heures, salle 1007<br/> <strong>Loic Peyrot</strong> <em>Repetition soutenance de these</em> <br/> </p> <p> <a href="https://www.irif.fr/seminaires/sms/index" class="wikilink1" title="seminaires:sms:index" data-wiki-id="seminaires:sms:index">La syntaxe rencontre la sémantique</a><br/> Vendredi 28 octobre 2022, 14 heures, salle 1007<br/> <strong>Pablo Barenbaum</strong> <em>Proof Terms for Higher-Order Rewriting and Their Equivalence</em> <br/> </p> <p> <a href="https://www.irif.fr/seminaires/sms/index" class="wikilink1" title="seminaires:sms:index" data-wiki-id="seminaires:sms:index">La syntaxe rencontre la sémantique</a><br/> Mercredi 19 octobre 2022, 14 heures, salle 1007<br/> <strong>Adrienne Lancelot</strong> <em>Open Call-by-Value and Open Similarity</em> <br/> </p> </div> </div> <div class="level4"> </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=seminaires%3Asms%3Aindex&1732397514" width="2" height="1" alt="" /> </div> </body> </html>