脡cole de Printemps d'Informatique Th茅orique 2025

<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"><html xmlns="http://www.w3.org/1999/xhtml"> <head> <meta http-equiv="Content-Type" content="text/html; charset=utf-8" />  <link rel="icon" type="type/png" href="/img/favicon.png" /> <link href="https://epit2025.sciencesconf.org/feeds/rss" title="epit2025.sciencesconf.org : RSS" type="application/rss+xml" rel="alternate" /> <link href="https://epit2025.sciencesconf.org/feeds/atom" title="epit2025.sciencesconf.org : Atom" type="application/atom+xml" rel="alternate" /> <title>脡cole de Printemps d'Informatique Th茅orique 2025 - Sciencesconf.org</title> <script type="text/javascript"> //<![CDATA[ var lang = 'en'; var langs = ['fr', 'en']; //]]> </script><link rel="stylesheet" href="https://epit2025.sciencesconf.org/css/jquery/ui/jquery.ui.css?1.16.4" type="text/css" media="screen" /> <link rel="stylesheet" href="https://epit2025.sciencesconf.org/css/jquery/jquery.tipsy.css?1.16.4" type="text/css" media="screen" /> <link rel="stylesheet" href="https://epit2025.sciencesconf.org/css/conference/templates/base.css?1.16.4" type="text/css" media="screen" /> <link rel="stylesheet" href="https://epit2025.sciencesconf.org/css/conference/templates/template_980_centre_vertical.css?1.16.4" type="text/css" media="screen" /> <link rel="stylesheet" href="https://epit2025.sciencesconf.org/css/conference.css?1.16.4" type="text/css" media="screen" /> <link rel="stylesheet" href="https://epit2025.sciencesconf.org/data/css/skin.css" type="text/css" media="screen" /> <script type="text/javascript" src="https://epit2025.sciencesconf.org/js/jquery/jquery.js"></script> <script type="text/javascript" src="https://epit2025.sciencesconf.org/js/jquery/jquery.ui.js"></script> <script type="text/javascript" src="https://epit2025.sciencesconf.org/js/translation.php?lang=en"></script> <script type="text/javascript" src="https://epit2025.sciencesconf.org/js/jquery/jquery.json.js?1.16.4"></script> <script type="text/javascript" src="https://epit2025.sciencesconf.org/js/conference/form.js?1.16.4"></script> <script type="text/javascript" src="https://epit2025.sciencesconf.org/js/jquery/jquery.tipsy.js?1.16.4"></script> <script type="text/javascript" src="https://epit2025.sciencesconf.org/js/sciencesconf.js?1.16.4"></script> </head> <body>  <div id='template_external' class='site_position'>  <div id='template_wrapper' class='largeur_page'>  <div id='template_header' style="background:url('https://epit2025.sciencesconf.org/data/header/1200x680_sc_station_d_aussois_en_haute_maurienne_vanosieatd_cuvelier.jpg') no-repeat left top #ffffff;color:#000000"> <table style="border: 0; border-spacing: 0; border-collapse: collapse; padding: 0;"> <tr> <td class="tac vam"> <a href="/"><img src="https://epit2025.sciencesconf.org/img/conference/logo_sciences_conf.png" name="header_logo" id="header_logo" style='margin-right:30px'/></a> </td> <td class="tal vam"> <div id='header_title'><a href="/" style="color:#000000">EPIT 2025 : 脡cole de Printemps <br /> d'Informatique Th茅orique 2025 <br /> <br /> (Co)inductive & circular reasoning <br /> applied to programming, formal <br /> proofs and software verification <br /></a></div> <div id='header_subtitle'></div> <div id='header_wheredate'> 19-23 May 2025 Aussois (France) </div> </td> </tr> </table> </div>  <div id='template_link'> <table class="book_papers link_h"> <tr> <td class="tal vam">  <div class="language"> <span style="padding:0 2px"> <a href="/?forward-action=index&forward-controller=index&lang=fr"> <span style="padding: 5px; ">FR</span></a></span> <span style="padding:0 2px"> <a href="/?forward-action=index&forward-controller=index&lang=en"> <span style="padding: 5px; background-color: var(--violet-sc02); color: white;">EN</span></a></span> </div>  </td>   <td class="tar vam">  <div class='filariane_quicklogin'> <form action="/user/login" method="post"> <input type="hidden" name="conference" value="epit2025" /> <div class="btngrp"> <button type="submit" class="btn-login menu_niveau_1_on"> <img src="/img/user-w.png" style="width: 12px;"/> Login </button> <div class="dropdown"> <button class="dropbtn menu_niveau_1_on" type="button"><span class="caret"></span></button> <div class="dropdown-content"> <a href="/user/lost">Lost password ?</a> <a href="/user/createaccount" class="linkCreateUser">Create account</a> </div> </div> </div> </form> </div>  </td> </tr> </table> </div>  <table id='template_main' class="tpl_main_v"> <tr> <td class="tal vat" id='template_menu'><div id="menu" class="menu_v fll"> <div class='menu_cartouche'>Main menu</div> <div id='menu_public' class='menu mb_20'> <div class='sousmenu_cartouche'> <div class='menu_niveau_1_on menu_202003'><a href='/?lang=en' target='_self'>Home</a><input type="hidden" class="menu" value="202003.0" /></div> <div class='menu_niveau_1 menu_212627'><a href='/page/inscription?lang=en' target='_self'>Registration</a><input type="hidden" class="menu" value="212627.0" /></div> <div class='menu_niveau_1 menu_210347'><a href='/program?lang=en' target='_self'>Planning</a><input type="hidden" class="menu" value="210347.0" /></div> <div class='menu_niveau_1 menu_214494'><a href='/page/abstracts?lang=en' target='_self'>Course Abstracts</a><input type="hidden" class="menu" value="214494.0" /></div> <div class='menu_niveau_1 menu_202013'><a href='/resource/news?lang=en' target='_self'>News</a><input type="hidden" class="menu" value="202013.0" /></div> <div class='menu_niveau_1 menu_202195'><a href='/resource/acces?lang=en' target='_self'>Venue</a><input type="hidden" class="menu" value="202195.0" /></div> <div class='menu_niveau_1 menu_210568'><a href='/page/infos_pratiques?lang=en' target='_self'>Practical information</a><input type="hidden" class="menu" value="210568.0" /></div> <div class='menu_niveau_1 menu_210349'><a href='/page/epit?lang=en' target='_self'>About EPIT</a><input type="hidden" class="menu" value="210349.0" /></div> </div> </div> <div id='menu_gestion' class='menu mb_20'>  </div> <div id='menu_contact' class='menu' > <div class='menu_cartouche'>HELP</div> <div class='sousmenu_cartouche'> <div id="menu_mail" class='menu_niveau_1'> <script type="text/javascript" language="javascript">decrypt('rcvg2025@fpvraprfpbas.bet', 'mailContact');</script> <a id="mailContact" href="mailto:" >@ Contact</a> </div>  </div> </div> </div> </td> <td class="tal vat w_100" id='template_content'> <div id='wp_51681' class='widget'><p class='titre'>Description</p> <div class='widget-content'> <div><div id="header_title" style="text-align: center;"><span style="color: #99ccff; font-size: large;"><strong>(Co)inductive & circular reasoning </strong></span><br /><span style="color: #99ccff; font-size: large;"><strong>applied to programming, formal </strong></span><br /><span style="color: #99ccff; font-size: large;"><strong>proofs and software verification </strong></span></div> <div id="header_subtitle" style="text-align: center;"><span style="color: #99ccff; font-size: large;"><strong> </strong></span></div> <div id="header_wheredate" style="text-align: center;"><span style="color: #000000; font-size: medium;"><strong>19-23 May 2025 Aussois (France)</strong></span></div> <p style="text-align: justify;"> </p> <p style="text-align: justify;">Every year since 1973, EPIT, the French Spring School on Theoretical Computer Science, consists in an intensive research school in a field of TCS  which gathers senior academics as well as young researchers. EPIT 2025 will take place <strong>from may 19th to may 23rd 2025</strong> and will focus on a theme from logic, coinductive and circular reasoning, and its applications to programming, formal proofs and software verification.</p> <p style="text-align: justify;"> </p> <p style="text-align: justify;">Given the widespread nature of inductively defined data (integers, finite lists and trees, etc.), induction is one of the fundamental concepts in computer science, and the principles of induction are among its most important reasoning principles. As the dual concept of induction, coinduction allows for modeling and reasoning about infinite data and behaviors (finite or infinite lists, infinite words, streams, infinite trees, execution traces, bisimulations, etc.), and comes with its own reasoning principles.</p> <p style="text-align: justify;">While coinduction can reasonably be considered as fundamental as induction, this concept is not as widespread in the theoretical computer science community as induction, nor as well known: attention to coinduction is more recent, and the computer science community is far less familiar with coinduction than with induction.</p> <p style="text-align: justify;">Various forms of inductive and coinductive reasoning have been developed since the beginning of the century, including logically grounded "circular reasoning," related to infinite descent reasoning, initially popularized by Fermat in mathematics. Our project, with this school, is to explore the potential applications of these new forms of (co)inductive reasoning — and in particular circular proofs, which constitute a correct form of circular reasoning — for (i) typed programming languages, (ii) proof assistants, and (iii) software verification techniques, in order to highlight the convergence of methods from these diverse fields that are typically considered distinct.</p> <p style="text-align: justify;"> </p> <p style="text-align: justify;">This year topic aims at gathering members of those three communities to evidence shared perspectives and, if possible, foster the emergence of joint research interests. In order to take into account the diversity of the targeted audience, the school will start with half-a-day of lecture reviewing background of those domains recalling the prior knowledge, it will then explore the fundamental concepts and tools of the topic before, in a third part, providing more advanced research perspectives.</p> <p style="text-align: justify;"> </p> <p style="text-align: justify;">Informations on registration can be found <a href="https://epit2025.sciencesconf.org/page/inscription">on the dedicated page</a>.</p> <p style="text-align: justify;"> </p></div> </div></div><div id='wp_51683' class='widget'><p class='titre'>Program</p> <div class='widget-content'> <div><p><strong><span style="text-decoration: underline;">This programme is provisional:</span> titles of the courses may be updated as the syllabus of each course is published by the end of february.<br /></strong></p> <p><em><strong>STARTING BLOCK:</strong></em></p> <p><span>COURSE 0: <em>Back to basics</em> – Background course as a school starter. A review of the basic concepts underlying the school (in proof theory, type theory, verification and model-checking, fixed-points, coinductive reasoning, basics of proof assistants, etc.)</span></p> <p><span> </span></p> <p><em><strong>FUNDAMENTAL BLOCK:</strong></em></p> <p>COURSE 1: <em>The μ-calculus and its proof-theory</em> by Bahareh Afshari (University of Gothenburg, Sweden)</p> <p>COURSE 2: <em>Basics of category theory, algebras and coalgebras </em><em>by</em> Farzad Jafarrahmani (Lagrange Center, France) and Daniela Petri葯an (Université Paris Cité, France)</p> <p>COURSE 3: <em>Automata on infinite structures</em> by Karoliina Lehtinen (CNRS, France)</p> <p><em>COURSE 4: Circular and non wellfounded proofs: expressiveness and semantics</em></p> <ul> <li><em>Expressiveness of cyclic proofs </em>by Anupam Das (University of Birmingham, UK)</li> <li><em>Denotational semantics of (co)inductive types and fixed-point logics </em>by Farzad Jafarrahmani  (Lagrange Center, France) </li> </ul> <p><strong> </strong></p> <p><em><strong>FROM ABSTRACTIONS TO APPLICATIONS:</strong></em></p> <p>COURSE 5: <em>Higher-order languages, Categories and Automata </em></p> <ul> <li><em>Coalgebraic and functorial approaches to automata theory </em>by Daniela Petri葯an (Université Paris Cité, France)</li> <li><em>Higher-order languages and parity automata</em> by Paul-André Melliès (CNRS, France)</li> </ul> <p>COURSE 6: <span style="color: #000000;"><em>Bisimulation and coinductive types in the Rocq proof assistant</em> by D</span>amien Pous (CNRS, France) and Yannick Zakowski (INRIA, France)</p> <p>COURSE 7: <em><span style="color: #000000;"><em><em>Software Verification via Fixed-Point Logics: Constraint Solving, Cyclic-Proof Search, and Strategy Synthesis </em></em></span></em>by Hiroshi Unno (Tohoku University, Japan)</p> <p>COURSE 8: <em>Guarded recursive types </em>by Daniel Gratzer (Aarhus University, Denmark) and Adrien Guatto (Université Paris Cité, France)</p> <p> </p></div> </div></div><div id='wp_51680' class='widget'><p class='titre'>Organizers</p> <div class='widget-content'> <div><ul> <li>Guilhem Jaber (LS2N)</li> <li>Denis Kuperberg (LIP)</li> <li>Luigi Santocanale (LIS)</li> <li>Alexis Saurin (IRIF)</li> </ul> <p> </p></div> </div></div><div id='wp_53886' class='widget'><p class='titre'>Scientific committee</p> <div class='widget-content'> <div><ul> <li>Bahareh Afshari (U. Gothenburg)</li> <li>Zena Ariola (U. Oregon)</li> <li>Anupam Das (U. Birmingham)</li> <li>Guilhem Jaber (LS2N)</li> <li>Denis Kuperberg (LIP)</li> <li>Daniela Petrisan (IRIF)</li> <li>Luigi Santocanale (LIS)</li> <li>Alexis Saurin (IRIF)</li> </ul> <p><br /><br /></p></div> </div></div><div id='wp_53887' class='widget'><p class='titre'>Sponsors</p> <div class='widget-content'> <div><p>EPIT 2025 is sponsored by:</p> <ul> <li>ANR</li> <li>CNRS</li> <li>IRIF</li> </ul> <p> </p></div> </div></div><div id='wp_51682' class='widget'><p class='titre'>Contact</p> <div class='widget-content'> <div><p>For any questions about the school, please send an email to <a href="mailto:epit2025@sciencesconf.org">epit2025@sciencesconf.org</a>.</p></div> </div></div> </td> </tr> </table>  <div id='template_foot'> <div class="tar"> <table class="book_papers"> <tr> <td class="tal vam w_30"> <span class="online_users"> Online user: <b>1</b> </span> </td> <td class="tac vam w_30"> <a href="https://epit2025.sciencesconf.org/feeds/rss" class="linkrss">RSS Feed</a> | <a href=https://portal.sciencesconf.org/index/rgpd class="texte_trebuchet_12_normal_grisfonce">Privacy</a> | <a href=https://portal.sciencesconf.org/index/rgaa class="texte_trebuchet_12_normal_grisfonce">Accessibility</a> </td> <td class="tar vam"> <a href="http://ccsd.cnrs.fr" target='_blank'><img src="/img/ccsd.png" title="CCSD" /></a> <a href="http://www.sciencesconf.org/" target='_blank'><img src="/img/favicon-g.png" class="logo_sc" title="Sciencesconf.org" /></a> </td> </tr> </table> </div> </div> </div> </div> <div id="template_center"></div>  <div id='popup_dialog' class="alert none"></div> <div id='popup_alert' class="alert none"></div> <div id='popup_confirm' class="alert none"></div> <div id='loading' class='none'> <div class="msgbox"> <div> <span id="loading_img"><img src="https://epit2025.sciencesconf.org/img/conference/load.gif" class="tac mr_10"/></span>Loading... </div> </div> </div>  <script type="text/javascript"> var pkBaseURL = "https://piwik-sc.ccsd.cnrs.fr/" ; document.write(unescape("%3Cscript src='" + pkBaseURL + "piwik.js' type='text/javascript'%3E%3C/script%3E")); </script><script type="text/javascript"> try { var piwikTracker = Piwik.getTracker(pkBaseURL + "piwik.php", 15502); piwikTracker.trackPageView(); piwikTracker.enableLinkTracking(); } catch( err ) {} </script> <noscript><p><img src="https://piwik-sc.ccsd.cnrs.fr/piwik.php?idsite=15502" alt="" /></p> </noscript> </body> </html>

CINXE.COM

脡cole de Printemps d'Informatique Th茅orique 2025 - Sciencesconf.org