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>Théorie des types et réalisabilité</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,types,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/types/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/types/index"/> <link rel="alternate" type="text/plain" title="Wiki balise" href="https://www.irif.fr/_export/raw/seminaires/types/index"/> <link rel="canonical" href="https://www.irif.fr/seminaires/types/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:types';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:types:index","namespace":"seminaires:types","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:types: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"> <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 active"> <a href="https://www.irif.fr/seminaires/types/index" class="wikilink1" title="seminaires:types:index" data-wiki-curid="true">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/types/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/types/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/types/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:types:indexheader" id="plugin_include__seminaires__types__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/types/0_pageid" class="wikilink2" title="seminaires:types:0_pageid" rel="nofollow" data-wiki-id="seminaires:types: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/types/0_pageid" class="wikilink2" title="seminaires:types:0_pageid" rel="nofollow" data-wiki-id="seminaires:types: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="theorie_des_types_et_realisabilite" class=" page-header pb-3 mb-4 mt-5">Théorie des types et réalisabilité</h2> <div class="level2"> <p> <br/> </p> </div> <h4 id="jour_heure_et_lieu">Jour, heure et lieu</h4> <div class="level4"> <p> Le mercredi à 14h, salle 1007 </p> <p> Le <a href="http://www.irif.fr/_media/ical/types.ics" class="urlextern" title="http://www.irif.fr/_media/ical/types.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="http://pauillac.inria.fr/~herbelin" class="urlextern" title="http://pauillac.inria.fr/~herbelin" rel="ugc nofollow">Hugo Herbelin</a><br/> <a href="https://www.irif.fr/~mellies" class="urlextern" title="https://www.irif.fr/~mellies" rel="ugc nofollow">Paul-André Melliès</a><br/> </p> </div> </div> </div> <p> Pour recevoir les annonces, s'abonner <a href="https://listes.u-paris.fr/wws/info/gt.rea-tt.irif" class="urlextern" title="https://listes.u-paris.fr/wws/info/gt.rea-tt.irif" rel="ugc nofollow">ici</a>. </p> </div> <p> <br/> </p> <h3 class="sectionedit3 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_2023">Année 2023</h4> <div class="level4"> </div> <div class="plugin_include_content plugin_include__seminaires:types:types2023" id="plugin_include__seminaires__types__types2023"> <div class="level4"> <p> <a href="https://www.irif.fr/seminaires/types/index" class="wikilink1" title="seminaires:types:index" data-wiki-id="seminaires:types:index">Théorie des types et réalisabilité</a><br/> Mardi 18 juillet 2023, 14 heures, Salle 147 (bâtiment Olympe de Gouge)<br/> <strong>Paige North</strong> (Utrecht University) <em>Coinductive control of inductive data types</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b17-3155"><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="b17-3155"><div class="bs-wrap bs-wrap-well well well-sm"> In classical programming language theory, characterizing data types as initial algebras of an endofunctor that represents a specification of the data types is an important tool. In this work, we observe that the category of algebras of such an endofunctor is often enriched in its category of coalgebras. This enrichment carries strictly more information than the traditional, unenriched category. For example, when considering the endofunctor whose initial algebra is the natural numbers, we find that the enrichment encodes a notion of `partial' homomorphism, while the unenriched category encodes only `total' homomorphisms. We can also leverage this extra information to generalize the notion of initial algebras, following the theory of weighted limits. </div> </div> </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:types:types2022" id="plugin_include__seminaires__types__types2022"> <div class="level4"> <p> <a href="https://www.irif.fr/seminaires/types/index" class="wikilink1" title="seminaires:types:index" data-wiki-id="seminaires:types:index">Théorie des types et réalisabilité</a><br/> Mercredi 14 décembre 2022, 14 heures, Salle 1007<br/> <strong>Rémy Cerda</strong> (Institut de Mathématiques de Marseille, Université Aix-Marseille) <em>Non encore annoncé.</em> <br/> </p> <p> <a href="https://www.irif.fr/seminaires/types/index" class="wikilink1" title="seminaires:types:index" data-wiki-id="seminaires:types:index">Théorie des types et réalisabilité</a><br/> Mercredi 16 novembre 2022, 14 heures, Salle 1007<br/> <strong>Hugo Férée Et Sam Van Gool</strong> <em>A formally verified construction of propositional quantifiers for intuitionistic logic</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b17-3156"><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="b17-3156"><div class="bs-wrap bs-wrap-well well well-sm"> A surprising result of Pitts (1992) says that propositional quantifiers are definable internally in intuitionistic propositional logic (IPC) - this result is commonly known as the uniform interpolation theorem for IPC. We recently completed a formalization of Pitts' result in the Coq proof assistant, and thus a verified implementation of the propositional quantifiers. Our Coq formalization in addition allowed us to extract an OCaml program that computes propositional formulas that realize intuitionistic versions of ∃p φ and ∀p φ from p and φ, and runs quickly on examples. <p> In this talk, we will give some background for the result, and I will make some points about its proof that we clarified during its implementation, which also give some new insights about the “pen-and-paper” proof. In our implementation, as in Pitts' original proof, the propositional quantifiers are defined by a mutual induction based on Dyckhoff's proof calculus LJT. The correctness of the construction is then proved by an induction on the size of an LJT-proof. The techniques used and lessons learned from our implementation may also be of more general interest for verified implementations of other proof-theoretic results. </div> </p> </div> <p> <a href="https://www.irif.fr/seminaires/types/index" class="wikilink1" title="seminaires:types:index" data-wiki-id="seminaires:types:index">Théorie des types et réalisabilité</a><br/> Vendredi 21 octobre 2022, 10 heures, Salle 1007<br/> <strong>Thorsten Altenkirch</strong> <em>Do we need classical logic?</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b17-3157"><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="b17-3157"><div class="bs-wrap bs-wrap-well well well-sm"> How should we make sense of the fact that classical mathematics officially is based on ZFC, but people that formalize classical mathematics in the computer use a foundation different from ZFC, e.g. type theory in the case of Lean ormalization? </div> </div> <p> <a href="https://www.irif.fr/seminaires/types/index" class="wikilink1" title="seminaires:types:index" data-wiki-id="seminaires:types:index">Théorie des types et réalisabilité</a><br/> Mercredi 19 octobre 2022, 14 heures, Salle 1007<br/> <strong>Peter Dybjer</strong> <em>On Generalized Algebraic Theories and Categories with Families</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b17-3158"><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="b17-3158"><div class="bs-wrap bs-wrap-well well well-sm"> We give a syntax independent formulation of finitely presented generalized algebraic theories as initial objects in categories of categories with families (cwfs) with extra structure. To this end we simultaneously define the notion of a presentation Σ of a generalized algebraic theory and the associated category CwF_Σ of small cwfs with a Σ-structure and cwf-morphisms that preserve Σ-structure on the nose. Our definition refers to the purely semantic notion of uniform family of contexts, types, and terms in CwF_Σ. Furthermore, we show how to syntactically construct an initial cwf with a Σ-structure. This result can be viewed as a generalization of Birkhoff’s completeness theorem for equational logic. It is obtained by extending Castellan, Clairambault, and Dybjer’s construction of an initial cwf. We provide examples of generalized algebraic theories for monoids, categories, categories with families, and categories with families with extra structure for some type formers of Martin-Lo ̈f type theory. The models of these are internal monoids, internal categories, and internal categories with families (with extra structure) in a small category with families. Finally, we show how to extend our definition to some generalized algebraic theories that are not finitely presented, such as the theory of contextual cwfs. </div> </div> <p> Also on <a href="https://galene.org:8443/group/herbelin/gt-rea-tt" class="urlextern" title="https://galene.org:8443/group/herbelin/gt-rea-tt" rel="ugc nofollow">https://galene.org:8443/group/herbelin/gt-rea-tt</a> (no password) </p> <p> <a href="https://www.irif.fr/seminaires/types/index" class="wikilink1" title="seminaires:types:index" data-wiki-id="seminaires:types:index">Théorie des types et réalisabilité</a><br/> Mercredi 19 octobre 2022, 15 heures 15, Salle 1007<br/> <strong>Ambrus Kaposi</strong> <em>Formalisation of type theory in type theory using quotient-inductive-inductive-recursive types</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b17-3159"><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="b17-3159"><div class="bs-wrap bs-wrap-well well well-sm"> In 2006, Nils Anders Danielsson formalised type theory in Agda using inductive-inductive-recursive types (IIRTs) before those types were understood. In 2009, James Chapman formalised type theory in Agda using inductive-inductive types (IITs) before the term “induction-induction” was coined. In 2016, Thorsten and I formalised type theory in Agda using quotient inductive-inductive types (QIITs) before a formal definition of QIITs was given. Cubical Agda now supports quotient inductive-inductive-recursive types (QIIRTs). We don't yet understand QIIRTs, so it is time to formalise the syntax of type theory using them! This is work in progress. </div> </div> <p> Also on <a href="https://galene.org:8443/group/herbelin/gt-rea-tt" class="urlextern" title="https://galene.org:8443/group/herbelin/gt-rea-tt" rel="ugc nofollow">https://galene.org:8443/group/herbelin/gt-rea-tt</a> (no password) </p> <p> <a href="https://www.irif.fr/seminaires/types/index" class="wikilink1" title="seminaires:types:index" data-wiki-id="seminaires:types:index">Théorie des types et réalisabilité</a><br/> Mercredi 12 octobre 2022, 14 heures, Salle 3052<br/> <strong>Félix Castro</strong> <em>An interpretation (by parametricity) of E-HA^ω inside HA^ω</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b17-3160"><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="b17-3160"><div class="bs-wrap bs-wrap-well well well-sm"> HA^ω (Higher Type Arithmetic) is a first order many sorted theory. It is a conservative extension of HA (Heyting Arithmetic a.k.a the intuitionistic version of Peano Arithmetic) obtained by extending the syntax of terms to all the System T : the objects of interest here are the functionals of “higher types”. While equality between natural numbers is well understood (it is canonical and decidable), how equality between functionals can be defined ? From this question, different versions of HA^ω arise : an extensional version (E-HA^ω) and an intentional version (I-HA^ω). <p> In this talk, we will see how the study of a (family of) partial equivalence relation(s indexed by the sorts of System T) leads us to design a translation (by parametricity) from E-HA^ω (HA^ω + extensional equality at all level) to HA^ω (where equality is only defined on natural numbers). </div> </p> </div> <p> <a href="https://www.irif.fr/seminaires/types/index" class="wikilink1" title="seminaires:types:index" data-wiki-id="seminaires:types:index">Théorie des types et réalisabilité</a><br/> Mercredi 6 juillet 2022, 14 heures, Salle 1007<br/> <strong>James Lipton</strong> (Wesleyan Univ., USA) <em>CUT ELIMINATION in Higher-Order with (HO) constraints</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b17-3161"><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="b17-3161"><div class="bs-wrap bs-wrap-well well well-sm"> We will present a system of Intensional Higher-Order Intuitionistic Logic with Higher-Order Saraswat Constraints, hoI(C). The Logic and its variants were developed by Artalejo, Nieva, Leach (Madrid), and subsequently by Lipton, Nieva and Hermant, the original aim being to add constraints to a lambda-Prolog style language. <p> If constraints are unrestricted, cut-elimination is easily shown to fail, because of the way the system handles equality rules. Our work studies conditions on the constraint system C that guarantee cut-elimination. The techniques used are based on Takahashi, Prawitz ande Andrews' work in classical type theory, Lipton and DeMarco for intuitionistic type theory, with ideas developed by Hermant for Logique Modulo, Hermant and Lipton for Logic with sequent axioms, as well as cut-elimination techniques due to Okada and Maehara. </p> <p> We will briefly discuss Kripke and HA semantics for these calculi, with some remarks on fibrational semantics developed by the speaker with Gianluca Amato (Pescara, Italy) if time permits! </p> <p> This will be a blackboard talk (with maybe a few slides) and will include work in progress! </div> </p> </div> </div> </div> <div class="level4"> <p> <br/> </p> </div> <h4 id="annee_2021">Année 2021</h4> <div class="level4"> </div> <div class="plugin_include_content plugin_include__seminaires:types:types2021" id="plugin_include__seminaires__types__types2021"> <div class="level4"> <p> <a href="https://www.irif.fr/seminaires/types/index" class="wikilink1" title="seminaires:types:index" data-wiki-id="seminaires:types:index">Théorie des types et réalisabilité</a><br/> Mercredi 8 décembre 2021, 14 heures, Salle 1007<br/> <strong>Federico Olimpieri</strong> (Université de Leeds) <em>Categorifying Intersection Types</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b17-3162"><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="b17-3162"><div class="bs-wrap bs-wrap-well well well-sm"> We study a family of distributors-induced bicategorical models of lambda-calculus, proving that they can be syntactically presented via intersection type systems. We first introduce a class of 2-monads whose algebras are monoidal categories modelling resource management. We lift these monads to distributors and define a parametric Kleisli bicategory, giving a sufficient condition for its cartesian closure. In this framework we define a proof-relevant semantics: the interpretation of a term associates to it the set of its typing derivations in appropriate systems. We prove that our model characterize solvability, adapting reducibility techniques to our setting. We conclude by describing two examples of our construction. </div> </div> <p> <a href="https://www.irif.fr/seminaires/types/index" class="wikilink1" title="seminaires:types:index" data-wiki-id="seminaires:types:index">Théorie des types et réalisabilité</a><br/> Mercredi 24 février 2021, 14 heures, online (<a href="https://bbb-front.math.univ-paris-diderot.fr/recherche/hug-a7x-lga-hy7" class="urlextern" title="https://bbb-front.math.univ-paris-diderot.fr/recherche/hug-a7x-lga-hy7" rel="ugc nofollow">https://bbb-front.math.univ-paris-diderot.fr/recherche/hug-a7x-lga-hy7</a>)<br/> <strong>Elaine Pimentel</strong> (UFRN - Brazil) <em>On linear logic, modalities and frameworks</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b17-3163"><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="b17-3163"><div class="bs-wrap bs-wrap-well well well-sm"> We start by presenting a local system for linear logic (LL) based on linear nested sequents. Relying on that system, we propose a general framework for modularly describing systems combining, coherently, substructural behaviors inherited from LL with simply dependent multimodalities. This class of systems includes linear, elementary, affine, bounded and subexponential linear logics and extensions of multiplicative additive linear logic (MALL) with normal modalities, as well as general combinations of them. <p> We then move to the question of giving an interpretation to subexponentials. We will show a game interpretation of affine linear logic with subexponentials, viewing the game as a playground for illuminating semantic intuitions underlying resource conscious reasoning. Interestingly enough, this led to the proposal of new sequent systems for capturing the notions of costs and budget in a fragment of linear logic with subexponentials, thus opening new possibilities for analysing the problem of comparing proofs. </p> <p> We finish the talk by showing a computational interpretation of subexponentials in the process-as-formula fashion, where process constructors are mapped to logical connectives and computational steps are related to proof steps. In particular, we will show in detail the role of pre-orders in subexponentials for the adequate specification of different modalities in concurrent systems, such as time, space, epistemic and preferences. We end with a discussion about which new models of computation should arise from the extension of the concept of modality in linear logic. </div> </p> </div> </div> </div> <div class="level4"> <p> <br/> </p> </div> <h4 id="annee_2020">Année 2020</h4> <div class="level4"> </div> <div class="plugin_include_content plugin_include__seminaires:types:types2020" id="plugin_include__seminaires__types__types2020"> <div class="level4"> <p> <a href="https://www.irif.fr/seminaires/types/index" class="wikilink1" title="seminaires:types:index" data-wiki-id="seminaires:types:index">Théorie des types et réalisabilité</a><br/> Mercredi 16 décembre 2020, 14 heures 30, Online (<a href="https://bbb-front.math.univ-paris-diderot.fr/recherche/hug-a7x-lga-hy7" class="urlextern" title="https://bbb-front.math.univ-paris-diderot.fr/recherche/hug-a7x-lga-hy7" rel="ugc nofollow">https://bbb-front.math.univ-paris-diderot.fr/recherche/hug-a7x-lga-hy7</a>)<br/> <strong>Pierre Pradic</strong> (University of Oxford) <em>Implicit automata in λ-calculi</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b17-3164"><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="b17-3164"><div class="bs-wrap bs-wrap-well well well-sm"> The talk will be based on joint work with Lê Thành Dũng (Tito) Nguyễn (<a href="https://arxiv.org/pdf/2008.01050.pdf" class="urlextern" title="https://arxiv.org/pdf/2008.01050.pdf" rel="ugc nofollow">https://arxiv.org/pdf/2008.01050.pdf</a>). <p> This work is part of an exploration of the expressiveness of the simply-typed λ-calculus (STLC) and related substructural variants (linear, affine, planar) using Church encodings of datatypes. More specifically, we are interested in the connection with automata theory for string transductions and languages. </p> <p> After introducing and motivating the problems using Hillebrand and Kanellakis' result stating that the classes of STLC-definable and regular languages coincide, I will discuss refinements we obtained for linear λ-calculi. I will focus on a correspondence with functions computed by copyless streaming string transducers (SSTs), and particularly on the ingredients of a completeness proof translating λ-terms to transducers. This will involve the notions of categorical automata as introduced by Colcombet and Petrisan, categorical models of linear logic and free completions, as well as automata-theoretic techniques related to the composition and determinization of SSTs. </div> </p> </div> <p> <a href="https://www.irif.fr/seminaires/types/index" class="wikilink1" title="seminaires:types:index" data-wiki-id="seminaires:types:index">Théorie des types et réalisabilité</a><br/> Lundi 14 décembre 2020, 14 heures, Online (<a href="https://bbb-front.math.univ-paris-diderot.fr/recherche/hug-a7x-lga-hy7" class="urlextern" title="https://bbb-front.math.univ-paris-diderot.fr/recherche/hug-a7x-lga-hy7" rel="ugc nofollow">https://bbb-front.math.univ-paris-diderot.fr/recherche/hug-a7x-lga-hy7</a>)<br/> <strong>Armaël Guéneau</strong> (Aarhus University) <em>Mechanized Program Verification on a Capability Machine in the Presence of Untrusted Code</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b17-3165"><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="b17-3165"><div class="bs-wrap bs-wrap-well well well-sm"> A capability machine is a kind of CPU which supports fine-grained privilege separation using capabilities (a pointer carrying a certain amount of authority). In this talk, I will present a methodology for verifying the functional correctness of capability machine programs that call (or are called by) unknown and potentially malicious code. The key aspects to the approach is a program logic for reasoning about known code, and a logical relation which provides a specification for unknown code. I will then hint at how we extend this methodology to reason about a secure calling convention enforcing a secure stack policy and the well-bracketedness of function calls. <p> This work has been entirely mechanized in Coq using the Iris framework: </p> <pre class="code">https://github.com/logsem/cerise https://github.com/logsem/cerise-stack</pre> <p> </div> </p> </div> </div> </div> <div class="level4"> <p> <br/> </p> </div> <h4 id="annee_2019">Année 2019</h4> <div class="level4"> </div> <div class="plugin_include_content plugin_include__seminaires:types:types2019" id="plugin_include__seminaires__types__types2019"> <div class="level4"> <p> <a href="https://www.irif.fr/seminaires/types/index" class="wikilink1" title="seminaires:types:index" data-wiki-id="seminaires:types:index">Théorie des types et réalisabilité</a><br/> Mercredi 11 décembre 2019, 14 heures, Salle 1007<br/> <strong>Danny Gratzer</strong> <em>Type Theory à la Mode</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b17-3166"><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="b17-3166"><div class="bs-wrap bs-wrap-well well well-sm"> Modalities have proved to be a recurring phenomenon in type theories, arising in both mathematical and computational contexts. For instance, recent work on cubical type theory has simplified the construction of univalent universes using the internal type theory of cubical sets supplemented with a comonad. On the other hand, guarded type theory has provided an account of coinduction using a handful of modalities. <p> Despite the wide variety of uses, a general framework for modal dependent type theories has still proven elusive. Each modal situation requires a handcrafted type theory, and establishing the properties of these type theories requires a significant technical investment. </p> <p> In this work, we have attempted to isolate a class of modal situations which can be given a single uniform syntax and allow for the typical metatheorems of type theory to be proven once and for all. Our calculus takes a mode theory as a parameter (an abstract description of the collection of modes, the modalities between them, and the ways in which they interactions) and produces a full dependent type theory satisfying canonicity. </p> <p> Our approach generalizes the ideas latent in Nuyts, Vezzosi, and Devriese, and simplifies the forthcoming work by Licata, Shulman, and Riley on a subset of mode theories. This calculus is sufficiently flexible to model internal parametricity, guarded recursion, and even axiomatic cohesion. </div> </p> </div> <p> <a href="https://www.irif.fr/seminaires/types/index" class="wikilink1" title="seminaires:types:index" data-wiki-id="seminaires:types:index">Théorie des types et réalisabilité</a><br/> Mercredi 27 novembre 2019, 14 heures, Salle 1007<br/> <strong>Bas Spitters</strong> (Aarhus university) <em>Synthetic topology in Homotopy Type Theory for probabilistic programming</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b17-3167"><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="b17-3167"><div class="bs-wrap bs-wrap-well well well-sm"> The ALEA Coq library formalizes measure theory based on a variant of the Giry monad on the category of sets. This enables the interpretation of a probabilistic programming language with primitives for sampling from discrete distributions. Continuous distributions (e.g. over the reals) cannot be treated this way, as not all subsets are measurable. We propose the use of synthetic topology to model continuous distributions while staying close to ALEA's approach. This allows us to model the apWhile language used in easycrypt to model differential privacy. We study the initial sigma-frame and the corresponding induced topology on arbitrary sets. We define valuations and lower integrals on sets that takes into account these intrinsic topologies, and we prove versions of the Riesz and Fubini theorems. We then show how the Lebesgue valuation, and hence continuous distributions, can be constructed. By interpreting our synthetic results in the K2-realizability topos, we recover the valuations on topological domains used as the semantics for the augurv2 probabilistic language, which has been used for machine learning. <p> Joint work with Martin Bidlingmaier (Aarhus) and Florian Faissole (INRIA). </div> </p> </div> <p> <a href="https://www.irif.fr/seminaires/types/index" class="wikilink1" title="seminaires:types:index" data-wiki-id="seminaires:types:index">Théorie des types et réalisabilité</a><br/> Mercredi 18 septembre 2019, 14 heures, Salle 1007<br/> <strong>Karl Palmskog</strong> (The University of Texas at Austin) <em>mCoq: Mutation Proving for Analysis of Verification Projects</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b17-3168"><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="b17-3168"><div class="bs-wrap bs-wrap-well well well-sm"> Mutation analysis, which introduces artificial defects into software systems, is the basis of mutation testing, a technique widely applied to evaluate and enhance the quality of test suites. However, despite the deep analogy between tests and formal proofs, mutation analysis has seldom been considered in the context of deductive verification. We propose mutation proving, a technique for analyzing verification projects that use proof assistants. We implemented our technique for the Coq proof assistant in a tool dubbed mCoq. mCoq applies a set of mutation operators to Coq definitions of functions and datatypes, inspired by operators previously proposed for functional programming languages. mCoq then checks proofs of lemmas affected by operator application. To make our technique feasible in practice, we implemented several optimizations in mCoq such as parallel proof checking. We applied mCoq to several medium and large scale Coq projects, and recorded whether proofs passed or failed when applying different mutation operators. We then qualitatively analyzed the mutants, and found several examples of weak and incomplete specifications. For our evaluation, we made many improvements to serialization of Coq code and even discovered a notable bug in Coq itself, all acknowledged by developers. We believe mCoq can be useful both to proof engineers for improving the quality of their verification projects and to researchers for evaluating proof engineering techniques. <p> Joint work with Ahmet Celik, Marinela Parovic, Emilio Jésus Gallego Arias, and Milos Gligoric. </p> <p> Speaker bio: Karl Palmskog is a Research Fellow at The University of Texas at Austin. His research focuses on proof engineering techniques and verification of distributed systems using Coq. He was previously a postdoctoral researcher at University of Illinois at Urbana-Champaign, working on topics related to the actor model of message-passing concurrency. He obtained his PhD from KTH Royal Institute of Technology. </div> </p> </div> <p> Video available at <a href="https://youtu.be/S6b6OMFiDFA" class="urlextern" title="https://youtu.be/S6b6OMFiDFA" rel="ugc nofollow">https://youtu.be/S6b6OMFiDFA</a> Slides available at <a href="https://setoid.com/slides/irif-2019.pdf" class="urlextern" title="https://setoid.com/slides/irif-2019.pdf" rel="ugc nofollow">https://setoid.com/slides/irif-2019.pdf</a> </p> <p> <a href="https://www.irif.fr/seminaires/types/index" class="wikilink1" title="seminaires:types:index" data-wiki-id="seminaires:types:index">Théorie des types et réalisabilité</a><br/> Vendredi 24 mai 2019, 14 heures, Salle 1007<br/> <strong>Hugo Moeneclaey</strong> <em>Monoids up to Coherent Homotopy in Two-Level Type Theory</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b17-3169"><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="b17-3169"><div class="bs-wrap bs-wrap-well well well-sm"> When defining a monoid structure on an arbitrary type in HoTT, one should require a multiplication that is not only homotopy-associative, but also has an infinite tower of higher homotopies. For example in dimension two one should have a condition similar to Mac Lane’s pentagon for monoidal categories. We call such a monoid a monoid up to coherent homotopy. The goal of my internship in Stockholm was to formalize them in Agda. It is well-known that infinite towers of homotopies are hard to handle in plain HoTT, so we postulate a variant of two-level type theory, with a strict equality and an interval type. Then we adapt the set-theoretical treatment of monoids up to coherent homotopy using operads as presented by Clemens Berger and Ieke Moerdijk [1,2]. <p> Our main results are: (a) Monoids up to coherent homotopy are invariant under homotopy equivalence (b) Loop spaces are monoids up to coherent homotopy. </p> <p> In this talk I will present the classical theory of monoids up to coherent homotopy, and indicates how two-level type theory can be used to formalize it. </p> <p> References </p> <p> 1. Axiomatic homotopy theory for operads (arxiv.org/abs/math/0206094) </p> <p> 2. The Boardman-Vogt resolution of operads in monoidal model categories (arxiv.org/abs/math/0502155) </div> </p> </div> <p> Organisé conjointement avec le groupe de travail catégories supérieures, polygraphes, et homotopie. </p> <p> <a href="https://www.irif.fr/seminaires/types/index" class="wikilink1" title="seminaires:types:index" data-wiki-id="seminaires:types:index">Théorie des types et réalisabilité</a><br/> Vendredi 29 mars 2019, 11 heures, Salle 3052<br/> <strong>Emilio J. Gallego Arias</strong> (MINES ParisTech) <em>Formalized Logic Programming, from Theory to Practice</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b17-3170"><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="b17-3170"><div class="bs-wrap bs-wrap-well well well-sm"> I will present past and ongoing work to develop mechanically-verified semantics and implementations of constraint logic programming. <p> (Constraint) logic programming is based on the utilization of proof search as a device for computation. The power that such a paradigm offers often comes at a cost for formal language research and implementation. Logic variables, unification, renaming apart, and proof search strategies are cumbersome to handle formally, and often specified informally or at the meta-logical level. </p> <p> In the first part of the talk I will describe algebraic semantics for proof search, based on the Tarski's relation algebras and Freyd's allegories. The main idea is to translate logic programs to _variable free_ relations; distribute relational algebras with quasi-projections do interpret defined predicates, whereas first-order rewriting simulates the traditional SLD proof search procedure. </p> <p> While the relation-based approach suffices to capture the proof search in a complete way, some rewriting steps are unsatisfactory from a more operational point of view, as they introduce extraneous terms in order to preserve certain global constraints. In an attempt to remedy this, we switch to the categorical version of relation algebra: allegories. </p> <p> In particular, for a signature Σ, we will interpret logic programs in the so-called Σ-allegories: distribute allegories whose conjunctive part is tabulated by a “Regular Lawvere Category”. </p> <p> In this setting, the single primitive of relation composition emcompasses unification, garbage collection, parameter passing, and environment creation and destruction. Tabulations play a crucial role, with their domain representing the set of live existential variables. Proof search is carried out by a notion of diagram rewriting, and is complete w.r.t. SLD, and satisfactory as form of abstract syntax for the program's execution. This new semantics paves the way to a formal extension of CLP with useful programming constructs. </p> <p> In the second part, I will shift focus to a different part of the logic programming spectrum, and describe ongoing efforts on formalizing logic programming engines over theories with finitary models on the Coq proof assistant. In particular, I will describe the implementation and verification of an engine for incremental model computation of a subset of Datalog that we have dubbed “Regular Datalog”. </p> <p> “Regular” Datalog stems from [Reutter,Romero,Vardi] Regular Queries, and it is of interest to the graph database community. The finite nature of the semantics of such programs allows to handle them quite naturally inside a constructive proof assistant, and to remain close to the usual mathematical notation. Borrowing from techniques from incremental view maintenance, we have developed a verified incremental model construction engine; to achieve a cost-effective mechanized proof of the soundness of the engine we had to develop a few notions specific to the ITP domain, such as generalized program signatures and a notion of relative satisfaction. We provide some preliminary benchmarks of the verified engine over realistic scenarios. </p> <p> To conclude, I will present some challenges that the practical utilization of proof assistants does face these days, and briefly discuss my ongoing work on this area. </div> </p> </div> </div> </div> <div class="level4"> <p> <br/> </p> </div> <h4 id="annee_2018">Année 2018</h4> <div class="level4"> </div> <div class="plugin_include_content plugin_include__seminaires:types:types2018" id="plugin_include__seminaires__types__types2018"> <div class="level4"> <p> <a href="https://www.irif.fr/seminaires/types/index" class="wikilink1" title="seminaires:types:index" data-wiki-id="seminaires:types:index">Théorie des types et réalisabilité</a><br/> Vendredi 18 mai 2018, 11 heures, Salle 3052<br/> <strong>Raphaël Cauderlier</strong> <em>Tactics and certificates in Meta Dedukti</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b17-3171"><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="b17-3171"><div class="bs-wrap bs-wrap-well well well-sm"> Tactics are often featured in proof assistants to simplify the interactive development of proofs by allowing domain-specific automation. Moreover, tactics are also helpful to check the output of automatic theorem provers because they can rebuild details that the provers omit. <p> We use meta-programming to define a tactic language for the Dedukti logical framework which can be used both for checking certificates produced by automatic provers and for developing proofs interactively. </p> <p> More precisely, we propose a dependently-typed tactic language for first-order logic in Meta Dedukti and an untyped tactic language built on top of the typed one. We show the expressivity of these languages on two applications: a transfer tactic and a resolution certificate checker. </div> </p> </div> <p> <a href="https://www.irif.fr/seminaires/types/index" class="wikilink1" title="seminaires:types:index" data-wiki-id="seminaires:types:index">Théorie des types et réalisabilité</a><br/> Mercredi 25 avril 2018, 14 heures, Salle 1007<br/> <strong>Hadrien Batmalle</strong> (IRIF) <em>Préservation de propriétés du modèle de départ en réalisbilité classique</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b17-3172"><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="b17-3172"><div class="bs-wrap bs-wrap-well well well-sm"> La réalisabilité classique permet d'interpréter des théories mathématiques classiques, comme la théorie des ensembles ZF, dans divers modèles de calcul (lambda-calcul avec continuations, domaines…) axiomatisés au moyen d'algèbres de réalisabilité. Elle produit ainsi des modèles de ces théories, de même qu'une technique bien connue, le forcing de Cohen, dont elle est en fait une généralisation. <p> Jusqu'ici, la réalisabilité classique a seulement été étudiée à partir d'un modèle de départ “raisonnable”, supposé au moins valider AC, voire même défini comme l'univers constructible. Dans cet exposé, on étudiera un analogue des “conditions d'antichaîne” du forcing nous permettant d'exporter certaines propriétés du modèle de départ au modèle de réalisabilité; et on l'appliquera pour obtenir des programmes réalisant Non DC (resp. Non CH) à partir de modèles de ZF bien choisis validant Non DC (resp. Non CH). </p> <p> — DC: axiome du choix dépendant CH: hypothèse du continu </div> </p> </div> <p> <a href="https://www.irif.fr/seminaires/types/index" class="wikilink1" title="seminaires:types:index" data-wiki-id="seminaires:types:index">Théorie des types et réalisabilité</a><br/> Lundi 19 mars 2018, 13 heures 15, 3052<br/> <strong>Adrien Guatto</strong> <em>A Generalized Modality for Recursion</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b17-3173"><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="b17-3173"><div class="bs-wrap bs-wrap-well well well-sm"> Nakano’s later modality allows types to express that the output of a function does not immediately depend on its input, and thus that computing its fixpoint is safe. This idea, guarded recursion, has proved useful in various contexts, from functional programming with infnite data structures to formulations of step-indexing internal to type theory. Categorical models have revealed that the later modality corresponds in essence to a simple reindexing of the discrete time scale. <p> Unfortunately, existing guarded type theories suffer from significant limitations for programming purposes. These limitations stem from the fact that the later modality is not expressive enough to capture precise input-output dependencies of functions. As a consequence, guarded type theories reject many productive definitions. Combining insights from guarded type theories and synchronous programming languages, we propose a new modality for guarded recursion. This modality can apply any well-behaved reindexing of the time scale to a type. We call such reindexings time warps. Several modalities from the literature, including later, correspond to fixed time warps, and thus arise as special cases of ours. </p> <p> We integrate our modality into a typed λ-calculus. We equip this calculus with an operational semantics, as well as an adequate denotational semantics in the topos of trees, a standard categorical model for guarded recursion. Building on top of categorical ideas, we describe an abstract type-checking algorithm whose completeness entails the coherence of both semantics. </div> </p> </div> <p> Attention, horaire et salle inhabituels </p> <p> <a href="https://www.irif.fr/seminaires/types/index" class="wikilink1" title="seminaires:types:index" data-wiki-id="seminaires:types:index">Théorie des types et réalisabilité</a><br/> Mercredi 14 mars 2018, 14 heures, Salle 1007<br/> <strong>Laura Fontanella</strong> (Institut de Mathématiques de Marseille) <em>L'Axiome du Choix dans la réalisabilité classique</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b17-3174"><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="b17-3174"><div class="bs-wrap bs-wrap-well well well-sm"> La réalisabilité fournit une interpretation des formules d'un système logique (ou d'une théorie) dans un modèle de calcul. Introduite par Kleene dans les années `40, la réalisabilité est née comme une interprétation des formules de l'arithmétique de Heyting par des ensembles d'indices de fonctions récursives. Avec J.-L. Krivine, la recherche en réalisabilité a évolué jusqu’à englober les axiomes de la théorie des ensembles. Les techniques développées par Krivine fournissent une méthode pour construire des modèles de la théorie des ensembles où tout énoncé de la théorie ZF plus l'Axiome du Choix Dépendant est réalisé. L'Axiome du Choix Dépendant, DC, est une version faible de l'Axiome du Choix; si et comment il serait possible de réaliser l'Axiome du Choix dans sa totalité reste une question ouverte. Nous allons considérer des principes intermédiaires: (1) le principe de partition, PP : étant donné deux ensembles A et B, s’il y a une surjection de A dans B, alors il y a une injection de B dans A; (2) le “Dual Cantor Bernstein theorem”, CB* : s’il y a une surjection de A dans B et une surjection de B dans A, alors A et B sont équipotents; (3) le principe de partition faible, WPP : s’il y a une surjection de A dans B et une injection de A dans B, alors A et B sont équipotents. Ces principes découlent de l'Axiome du Choix et sont plus forts que l'Axiome du Choix Dépendant. Cependant, on ne sait pas s'ils sont équivalents à l'Axiome du Choix et cela est un vieux problème ouvert formulé par B. Banacschewski et G. Moore en 1990. Est-il possible de construire un modèle de réalisabilité pour l'un de ces principes? Cette recherche peut aboutir à deux situations divergentes: soit on trouvera des modèles de réalisabilité pour ces principes où l’axiome du choix est également réalisé, soit on s’arrêtera à une étape donnée sur des modèles de réalisabilité où l’un de ces principes (ou tous) est réalisé, tandis que l’Axiome du Choix ne l’est pas, dans ce dernier cas on aurait alors montré que ces principes ne sont pas équivalents à l’Axiome du Choix et on aurait ainsi résolu le problème de Banacschewski-Moore. Je vous presenterai l'avancement de mes recherches dans ce domaine. </div> </div> <p> <a href="https://www.irif.fr/seminaires/types/index" class="wikilink1" title="seminaires:types:index" data-wiki-id="seminaires:types:index">Théorie des types et réalisabilité</a><br/> Mercredi 14 février 2018, 14 heures, Salle 1007<br/> <strong>Jérôme Siméon</strong> (Clause, Inc.) <em>Specifying and compiling domain specific languages using Coq: Three case studies</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b17-3175"><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="b17-3175"><div class="bs-wrap bs-wrap-well well well-sm"> Domain specific languages (DSL) can be well suited for certain business scenarios and be easier to learn for non-developers. We present our experience using the Coq proof assistant to support the formal specification and the compilation for three different DSLs: JRules (a language for business rules), SQL (a language for relational databases), and Jura (a language for legal contract). <p> We describe how each of those languages comes with its own challenges, and how they benefit differently from the use of a proof assistant. We also show how we could exploit their commonalities to build an optimizing and (partially) verified compiler for each of them. The core of that compiler uses traditional database representations (the Nested Relational Algebra and its corresponding Calculus) for optimization and code-generation. </p> <p> – Some of this work was done jointly with Joshua Auerbach, Martin Hirzel, Louis Mandel and Avi Shinnar as part of the Q*cert project (<a href="https://querycert.github.io/" class="urlextern" title="https://querycert.github.io/" rel="ugc nofollow">https://querycert.github.io/</a>). </div> </p> </div> <p> <a href="https://www.irif.fr/seminaires/types/index" class="wikilink1" title="seminaires:types:index" data-wiki-id="seminaires:types:index">Théorie des types et réalisabilité</a><br/> Mercredi 31 janvier 2018, 14 heures, Salle 1007<br/> <strong>Armaël Guéneau</strong> (Inria Paris) <em>A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b17-3176"><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="b17-3176"><div class="bs-wrap bs-wrap-well well well-sm"> I will present a framework for simultaneously verifying the functional correctness and the worst-case asymptotic time complexity of higher-order imperative programs. The framework is built on top of Separation Logic with Time Credits, embedded in the Coq proof assistant. I will formalize the O notation, which is key to enabling modular specifications and proofs, and cover the subtleties of the multivariate case, where the complexity of a program fragment depends on multiple parameters. I will propose a way of integrating complexity bounds into specifications, present lemmas and tactics that support a natural reasoning style, and illustrate their use with a collection of examples. </div> </div> <p> <a href="https://www.irif.fr/seminaires/types/index" class="wikilink1" title="seminaires:types:index" data-wiki-id="seminaires:types:index">Théorie des types et réalisabilité</a><br/> Mercredi 17 janvier 2018, 14 heures, Salle 1007<br/> <strong>Rodolphe Lepigre</strong> <em>Practical Curry-Style using Choice Operators, Local Subtyping and Circular proofs</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b17-3177"><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="b17-3177"><div class="bs-wrap bs-wrap-well well well-sm"> In a recent (submitted) work with Christophe Raffalli, we designed a rich type system for an extension of System F with subtyping. It includes primitive sums and products, existential types, (co-)inductive (sized) types, and it supports general recursion with termination checking. Despite its Curry-style nature, the system can be (and has been) implemented thanks to new techniques based on choice operators, local subtyping and circular proofs. During the talk, I will give you a flavour of these three ideas. In particular, I will show how choice operators can be used to get rid of free variables (and thus typing contexts), while yielding a clear semantics. I will show how local subtyping can be used to make the system syntax-directed. And I will show how circular proofs may be used to handle (co-)inductive types and (terminating) recursion. <p> References and links: - paper: <a href="http://lepigre.fr/files/docs/lepigre2017_subml.pdf" class="urlextern" title="http://lepigre.fr/files/docs/lepigre2017_subml.pdf" rel="ugc nofollow">http://lepigre.fr/files/docs/lepigre2017_subml.pdf</a> - implementation of the system: <a href="https://github.com/rlepigre/subml" class="urlextern" title="https://github.com/rlepigre/subml" rel="ugc nofollow">https://github.com/rlepigre/subml</a> - online interpreter and examples: <a href="https://rlepigre.github.io/subml" class="urlextern" title="https://rlepigre.github.io/subml" rel="ugc nofollow">https://rlepigre.github.io/subml</a> </div> </p> </div> </div> </div> <div class="level4"> <p> <br/> </p> </div> <h4 id="annee_2017">Année 2017</h4> <div class="level4"> </div> <div class="plugin_include_content plugin_include__seminaires:types:types2017" id="plugin_include__seminaires__types__types2017"> <div class="level4"> <p> <a href="https://www.irif.fr/seminaires/types/index" class="wikilink1" title="seminaires:types:index" data-wiki-id="seminaires:types:index">Théorie des types et réalisabilité</a><br/> Mercredi 20 décembre 2017, 14 heures, Salle 1007<br/> <strong>Ludovic Patey</strong> (ICJ, Lyon) <em>Introduction aux mathématiques à rebours</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b17-3178"><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="b17-3178"><div class="bs-wrap bs-wrap-well well well-sm"> Les mathématiques à rebours sont un domaine fondationnel qui vise à trouver les axiomes optimaux pour prouver les théorèmes de la vie de tous les jours. Elles se placent dans l'arithmétique du second ordre, avec une théorie de base, RCA, capturant informellement les “mathématiques calculables”. Nous reviendrons sur les justifications historiques des mathématiques à rebours, présenterons ses principales observations, ainsi que l'approche moderne des mathématiques à rebours comme formalisme de classification de phénomènes calculatoires. </div> </div> <p> <a href="https://www.irif.fr/seminaires/types/index" class="wikilink1" title="seminaires:types:index" data-wiki-id="seminaires:types:index">Théorie des types et réalisabilité</a><br/> Mercredi 6 décembre 2017, 14 heures, Salle 1007<br/> <strong>Francesco A. Genco</strong> (IRIF - TU Wien) <em>Typing Parallelism and communication through hypersequents</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b17-3179"><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="b17-3179"><div class="bs-wrap bs-wrap-well well well-sm"> We present a Curry–Howard correspondence for Gödel logic based on a simple natural deduction reformulating the hypersequent calculus for this logic. The resulting system extends simply typed λ-calculus by a symmetric higher-order communication mechanism between parallel processes. We discuss a normalisation procedure and several features of the parallel λ-calculus. Following A. Avron's 1991 thesis on the connection between hypersequents and parallelism, we also discuss the generalisation of the employed techniques for other intermediate logics. </div> </div> <p> <a href="https://www.irif.fr/seminaires/types/index" class="wikilink1" title="seminaires:types:index" data-wiki-id="seminaires:types:index">Théorie des types et réalisabilité</a><br/> Mercredi 29 novembre 2017, 14 heures, Salle 1007<br/> <strong>Guilhem Jaber</strong> (ENS Lyon) <em>A Trace Semantics for System F Parametric Polymorphism</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b17-3180"><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="b17-3180"><div class="bs-wrap bs-wrap-well well well-sm"> In this talk, we present a trace model for System F that captures Strachey parametric polymorphism. The model is built using operational nominal game semantics and enforces parametricity by using names. This model is used here to prove a conjecture of Abadi, Cardelli, Curien and Plotkin which states that Strachey equivalence implies Reynolds equivalence (i.e. relational parametricity) in System F. </div> </div> <p> <a href="https://www.irif.fr/seminaires/types/index" class="wikilink1" title="seminaires:types:index" data-wiki-id="seminaires:types:index">Théorie des types et réalisabilité</a><br/> Jeudi 16 mars 2017, 14 heures, Salle 1007<br/> <strong>Pierre-Marie Pédrot</strong> <em>An Effectful Way to Eliminate Addiction to Dependence</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b17-3181"><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="b17-3181"><div class="bs-wrap bs-wrap-well well well-sm"> We define a syntactic monadic translation of type theory, called the weaning translation, that allows for a large range of effects in dependent type theory, such as exceptions, non-termination, non-determinism or writing operation. Through the light of a call-by-push-value decomposition, we explain why the traditional approach fails with type dependency and justify our approach. Crucially, the construction requires that the universe of algebras of the monad forms itself an algebra. The weaning translation applies to a version of the Calculus of Inductive Constructions with a restricted version of dependent elimination, dubbed Baclofen Type Theory, which we conjecture is the proper generic way to mix effects and dependence. This provides the first effectful version of CIC, which can be implemented as a Coq plugin. </div> </div> </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%3Atypes%3Aindex&1732402000" width="2" height="1" alt="" /> </div> </body> </html>