<h2><CENTER>Monday 24 June, 2019 - Workshop </CENTER></h2><!-- [et_pb_line_break_holder] --> <p><!-- [et_pb_line_break_holder] --> <center><strong>Venue: <span style="color:red" > Technical University of Dortmund </span>ONLY on 24/06</strong></center><br> <!-- [et_pb_line_break_holder] --></p><!-- [et_pb_line_break_holder] --> <table style="text-align: center; border:1px"><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td width="10%"></td><!-- [et_pb_line_break_holder] --> <td width="44%"><strong>WPTE 2019</strong></td><!-- [et_pb_line_break_holder] --> <td width="46%"><strong>UNIF 2019</strong></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --><td>08:00 </td><!-- [et_pb_line_break_holder] --> <td colspan="2" style="background-color: #D1DBC1">Registration </td><!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted;"><!-- [et_pb_line_break_holder] --> <td style="width: 10%">09:00 - 10:00</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #D4C68D">Session 1<br> <strong>Chair:</strong>Vivek Nigam</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #D4C68D">Session 1<br><strong>Chair: </strong>Daniele Nantes</td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td></td><!-- [et_pb_line_break_holder] --> <td style="background-color: #FCF3CF"><strong>Invited Talk:</strong> External Termination Proofs for Isabelle/HOL<!-- [et_pb_line_break_holder] --> <BR><!-- [et_pb_line_break_holder] --> <i>Rene Thiemann, University of Innsbruck</i><!-- [et_pb_line_break_holder] --> </td><!-- [et_pb_line_break_holder] --> <td style="background-color: #fae5d3 "><strong>Invited Talk: </strong>Rethinking Unification Theory<br><i> Jörg Siekmann</i></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>10:00 - 10:30</td><!-- [et_pb_line_break_holder] --> <td colspan="2" style="background-color: #f8d9d3">Coffee Break</td><!-- [et_pb_line_break_holder] --> </tr> <!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>10:30 - 11:30</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #D4C68D">Session 2 <br><strong>Chair: </strong> David Sabel</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #D4C68D">Session 2<br><strong>Chair: </strong>TBD</td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td align="right">10:30 - 11:00</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #FCF3CF">Space Improvements for Total Garbage Collection<!-- [et_pb_line_break_holder] --> <br><i>Manfred Schmidt-Schauss and Nils Dallmeyer</i></td><!-- [et_pb_line_break_holder] --> <td style="background-color: #fae5d3 ">Unification of Multisets with Multiple Labelled Multiset Variables<br><i>Zan Naeem and Giselle Reis</i></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td align="right">11:00 - 11:30</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #FCF3CF">On Determinization of Inverted Grammar Programs via Context-Free<br><i>Naoki Nishida and Minami Niwa</i></td><!-- [et_pb_line_break_holder] --> <td style="background-color: #fae5d3 ">Formalising Nominal AC-Unification<br><i> Mauricio Ayala-Rincón, Maribel Fernández and Gabriel Ferreira Silva </i></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>11:30 - 12:30</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #D4C68D">Session 3<br><!-- [et_pb_line_break_holder] --> <strong>Chair: </strong>TBD</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #fae5d3 " >Parameters for Associative and Commutative Matching<br><i> Luis Bustamante, Ana Teresa Martins and Francicleber Ferreira</i></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td></td><!-- [et_pb_line_break_holder] --> <td style="background-color: #FCF3CF"><strong>Invited Talk: </strong> Strategic Graph Rewriting is an Interactive Modelling Framework<br><i>Maribel Fernandez, King's College London</i></td><!-- [et_pb_line_break_holder] --> <td style="background-color: #fae5d3 "><center><h4>12:00 - 12:30</h4></center>On Forward-closed and Sequentially-closed String Rewriting Systems <br><i>Yu Zhang, Paliath Narendran and Heli Patel </i></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>12:30 - 14:00</td><!-- [et_pb_line_break_holder] --> <td colspan="2" style="background-color: #f8d9d3">Lunch Break</td><!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>14:00 - 15:30</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #D4C68D">Session 4<br><strong>Chair: </strong>Naoki Nishida</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #D4C68D">Session 3<br><Storng>Chair: </Storng>TBD</td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td rowspan="2"></td><!-- [et_pb_line_break_holder] --> <td rowspan="2" style="background-color: #FCF3CF"><strong>Invited Talk: </strong>SQL for combinatori,al optimization problems and SMT - based solving by SQL transformation<br><i>Masahiko Sakai, Nagoya University</i></td><!-- [et_pb_line_break_holder] --> <td style="background-color: #fae5d3 "><center><h4>14:00 - 14:30</h4>Nominal Unification with Letrec and Environment-Variables<br><!-- [et_pb_line_break_holder] --> <i>Manfred Schmidt-Schauss and Yunus David Kerem Kutz </i><!-- [et_pb_line_break_holder] --> </center></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> <td style="background-color: #fae5d3 "><center><h4>14:30 - 15:00</h4></center>On Asymmetric Unification for the Theory of XOR with a Homomorphism<br><i>Christopher Lynch, Andrew M Marshall, Catherine Meadows, Paliath Narendran and Veena Ravishankar </i><br><!-- [et_pb_line_break_holder] --> <center><h4>15:00 - 15:30</h4></center> A Coq Formalization of Boolean Unification<br><i>Daniel Dougherty</i><!-- [et_pb_line_break_holder] --> </td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>15:30 - 16:00</td><!-- [et_pb_line_break_holder] --> <td colspan="2" style="background-color: #f8d9d3">Coffee Break</td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>16:00 - 17:00</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #D4C68D">Session 5<br><!-- [et_pb_line_break_holder] --> <strong>Chair: </strong>TBD</td><!-- [et_pb_line_break_holder] --> <TD style="background-color: #D4C68D">Session 4<br><strong>Chair: </strong>TBD</TD><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <TR style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <TD align="right">16:00 - 16:30</TD><!-- [et_pb_line_break_holder] --> <td style="background-color: #FCF3CF">Formalisation of Normalisation of the Simply Typed Lambda Calculus in F*<br><i>Sebastian Sturm</i></td><!-- [et_pb_line_break_holder] --> <td rowspan="2" style="background-color: #fae5d3 "><strong>Invited Talk: </strong>Maude strategies for narrowing<br><i> Narciso Martí-Oliet</i></td><!-- [et_pb_line_break_holder] --> </TR><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td align="right">16:30 - 17:00</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #FCF3CF">On Formalizing a Transformation of IMP Programs into Logically Constrained Term Rewriting Systems in Isabelle/HOL<br><i>Ryota Nakayama and Naoki Nishida</i></td><!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td></td><!-- [et_pb_line_break_holder] --> <td style="background-color: #FCF3CF "> </td><!-- [et_pb_line_break_holder] --> <td style="background-color: #fae5d3 "><center><h4>17:00 - 17:30</h4></center>Solving Proximity Constraints<br><i>Temur Kutsia and Cleo Pau</i><br><!-- [et_pb_line_break_holder] --> <center><h4>17:30</h4></center>Asymmetric Unification and Disunification for the theory of Abelian groups with a homomorphism(AGh)<i> Veena Ravishankar, Paliath Narendran and Kimberly Cornell</i><!-- [et_pb_line_break_holder] --> </td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --><!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> </table>

<table style="text-align: center; border:1px"><tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --><td>08:00</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #D1DBC1">Registration and opening</td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted;"><!-- [et_pb_line_break_holder] --> <td rowspan="2" style="width: 10%">09:00<br>-<br><!-- [et_pb_line_break_holder] --> 10:00</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #D4C68D"><p><strong>FSCD Invited Talk</strong><br>Chair: Dan Dougherty</p></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td style="background-color: #EBE2BF"><h5><em>Beniamino Accattoli</em></h5><!-- [et_pb_line_break_holder] --> <p><a href="#" class="popmake-604">A Fresh Look at the lambda-Calculus</a></p></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>10:00<br><!-- [et_pb_line_break_holder] --> -<br><!-- [et_pb_line_break_holder] --> 10:30</td><!-- [et_pb_line_break_holder] --> <td>Coffee Break</td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted; background-color: "><!-- [et_pb_line_break_holder] --> <td rowspan="5">10:30<br>-<br><!-- [et_pb_line_break_holder] --> 12:30</td><!-- [et_pb_line_break_holder] --> <td colspan="2" style="background-color: #BFBFBF"><p><strong>FSCD Theme: Lambda calculus</strong><Br>Chair: Ugo De'Liguoro</p></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td colspan="2" style="background-color: #E3E3E3"><em>Maciej Bendkowski<br><!-- [et_pb_line_break_holder] --> </em><a href="#" class="popmake-888">Towards the average-case analysis of substitution resolution in lambda-calculus</a></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td colspan="2" style="background-color: #E3E3E3"><em>Pierre Vial<br><!-- [et_pb_line_break_holder] --> </em><a href="#" class="popmake-892">Sequence Types for Hereditary Permutators</a></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td colspan="2" style="background-color: #E3E3E3"><em>Ugo Dal Lago and Thomas Leventis<br><!-- [et_pb_line_break_holder] --> </em><a href="#" class="popmake-894">On the Taylor Expansion of Probabilistic lambda-terms</a></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td colspan="2" style="background-color: #E3E3E3"><em>Simona Kašterović and Michele Pagani</em><br><!-- [et_pb_line_break_holder] --> <a href="#" class="popmake-896">The Discriminating Power of the Let-in Operator1in the Lazy Call-by-Name Probabilistic lambda-Calculus</a></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>12:30<br><!-- [et_pb_line_break_holder] --> -<br><!-- [et_pb_line_break_holder] --> 14:00</td><!-- [et_pb_line_break_holder] --> <td>Lunch Break</td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --><tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td rowspan="4">14:00<br>-<br><!-- [et_pb_line_break_holder] --> 15:30</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #BFBFBF"><strong>FSCD Theme: Calling Paradigms </strong><br>Chair: Paweł Urzyczyn</td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --><tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td style="background-color: #E3E3E3"><em>José Espírito Santo, Luís Pinto, and Tarmo Uustalu<br><!-- [et_pb_line_break_holder] --> </em><a href="#" class="popmake-898">Modal embeddings and calling paradigms</a></td><!-- [et_pb_line_break_holder] --></tr><!-- [et_pb_line_break_holder] --><tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td style="background-color: #E3E3E3"><p><em>Małgorzata Biernacka and Witold Charatonik<br><!-- [et_pb_line_break_holder] --> </em><a href="#" class="popmake-900">Deriving an Abstract Machine for Strong Call by Need</a></p></td><!-- [et_pb_line_break_holder] --></tr><!-- [et_pb_line_break_holder] --><tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td style="background-color: #E3E3E3"><p><em>Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski<br><!-- [et_pb_line_break_holder] --> </em><a href="#" class="popmake-902">Typed Equivalence of Effect Handlers and Delimited Control</a></p></td><!-- [et_pb_line_break_holder] --></tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>15:30<br><!-- [et_pb_line_break_holder] --> -<br><!-- [et_pb_line_break_holder] --> 16:00</td><!-- [et_pb_line_break_holder] --> <td>Coffee Break</td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td rowspan="5">16:00<br>-<br><!-- [et_pb_line_break_holder] --> 17:30</td><!-- [et_pb_line_break_holder] --> <td colspan="2" style="background-color: #BFBFBF"><strong>FSCD Theme: Logic and models of computation</strong><Br>Chair: Mauricio Ayala Rincon</td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td colspan="2" style="background-color: #E3E3E3"><em>Alejandro Díaz-Caro and Gilles Dowek<br><!-- [et_pb_line_break_holder] --> </em><a href="#" class="popmake-904">Proof Normalisation in a Logic Identifying Isomorphic Propositions</a></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td colspan="2" style="background-color: #E3E3E3"><em>Dominique Larchey-Wendling and Yannick Forster<br><!-- [et_pb_line_break_holder] --> </em><a href="#" class="popmake-906">Hilbert’s Tenth Problem in Coq</a></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td colspan="2" style="background-color: #E3E3E3"><em>Paulin Jacobé de Naurois<br><!-- [et_pb_line_break_holder] --> </em><a href="#" class="popmake-908">Pointers in Recursion: Exploring the<!-- [et_pb_line_break_holder] -->Tropics<!-- [et_pb_line_break_holder] --> </a></td></tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>19:00</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #D1C5DC"><strong>Reception</strong></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> </table>

<table style="text-align: center; border:1px"><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td width="10%"></td><!-- [et_pb_line_break_holder] --> <td width="49%"><strong>Main Conference</strong></td><!-- [et_pb_line_break_holder] --> <td width="41%"><strong>IFIP 2019</strong></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --><td>08:00</td><!-- [et_pb_line_break_holder] --> <td colspan="2" style="background-color: #D1DBC1">Registration</td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted; "><!-- [et_pb_line_break_holder] --> <td rowspan="2" style="width: 10%">09:00<br>-<br><!-- [et_pb_line_break_holder] --> 10:00</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #D4C68D"><p><strong>FSCD Invited Talk</strong><br>Chair: José Espírito Santo </p></td><!-- [et_pb_line_break_holder] --> <td style="background-color: #d0ece7 "><h4><center>08:30 - 9:00</center></h4>Welcome<br>Coffee Break</td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td style="background-color: #EBE2BF "><h5><em>Amy P. Felty</em></h5><!-- [et_pb_line_break_holder] --> <p><a href="#" class="popmake-616">A Linear Logical Framework in Hybrid</a></p></td><!-- [et_pb_line_break_holder] --> <td align="center" style="background-color: #d7bde2 "><strong>Session 1</strong><br><i>Cynthia Kop</i><br>Cons - Free Rewriting </td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>10:00<br><!-- [et_pb_line_break_holder] --> -<br><!-- [et_pb_line_break_holder] --> 10:30</td><!-- [et_pb_line_break_holder] --> <td colspan="2">Coffee Break</td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td rowspan="5">10:30<br>-<br><!-- [et_pb_line_break_holder] --> 12:30</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #BFBFBF"><p><strong>FSCD Theme: Types</strong><br>Chair: Thomas Ehrhard</p></td><!-- [et_pb_line_break_holder] --> <td align="center" style="background-color: #d7bde2 "><strong>Session 2</strong></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td style="background-color: #E3E3E3"><em>Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Marina Lenisa, and Ivan Scagnetto<br><!-- [et_pb_line_break_holder] --> </em><a href="#" class="popmake-910">lambda!-calculus, Intersection Types, and Involutions</a></td><!-- [et_pb_line_break_holder] --> <td align="center" style="background-color: #ebdef0 "><h4>10:30 - 11:30</h4><i>Rene Thiemann</i><br>Improved Certification of Complexity Proofs for Term Rewrite System</td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td style="background-color: #E3E3E3"><em>Luigi Liquori and Claude Stolze<br><!-- [et_pb_line_break_holder] --> </em><a href="#" class="popmake-912">The Delta-calculus: Syntax and Types</a></td><!-- [et_pb_line_break_holder] --> <td style="background-color: #ebdef0 "><h4>11:30 - 11:45</h4><i>Herman Geuvers</i><br>Informal Report on FSCD</td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td style="background-color: #E3E3E3"><em>Niccolò Veltri and Niels van der Weide<br><!-- [et_pb_line_break_holder] --> </em><a href="#" class="popmake-914">Guarded Recursion in Agda via Sized Types</a></td><!-- [et_pb_line_break_holder] --> <TD align="center" rowspan="2" style="background-color: #ebdef0 "><H4>11:45 - 12:30</H4>Report on IFIP</TD><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td style="background-color: #E3E3E3"><em>Ambrus Kaposi, Simon Huber, and Christian Sattler<br><!-- [et_pb_line_break_holder] --> </em><a href="#" class="popmake-916">Gluing for type theory</a></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>12:30<br><!-- [et_pb_line_break_holder] --> -<br><!-- [et_pb_line_break_holder] --> 14:00</td><!-- [et_pb_line_break_holder] --> <td colspan="2">Lunch Break</td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --><tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td rowspan="4">14:00<br>-<br><!-- [et_pb_line_break_holder] --> 15:30</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #BFBFBF"><strong>FSCD Theme: Homotopy Type Theory</strong><br>Chair: Herman Geuvers</td><!-- [et_pb_line_break_holder] --> <td align="center" style="background-color: #d7bde2 "><strong>Session 3</strong></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --><tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td style="background-color: #E3E3E3"><em>Thierry Coquand, Simon Huber, and Christian Sattler</em><br><!-- [et_pb_line_break_holder] --> <a href="#" class="popmake-918">Homotopy canonicity for cubical type theory</a></td><!-- [et_pb_line_break_holder] --> <td align="center" style="background-color: #ebdef0 "><h4>14:00 - 15:00</h4><i>Silvia Ghilezan</i><br>Denotational and Operational Preciseness of Subtyping</td><!-- [et_pb_line_break_holder] --></tr><!-- [et_pb_line_break_holder] --><tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td style="background-color: #E3E3E3"><p><em>Jonathan Sterling, Carlo Angiuli, and Daniel Gratzer</em><br><!-- [et_pb_line_break_holder] --> <a href="#" class="popmake-920">Cubical Syntax for Reflection-Free Extensional Equality</a></p></td><!-- [et_pb_line_break_holder] --> <td align="center" rowspan="2" style="background-color: #ebdef0 ">Report ISR </td><!-- [et_pb_line_break_holder] --></tr><!-- [et_pb_line_break_holder] --><tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td style="background-color: #E3E3E3"><p><em>Benedikt Ahrens, Dan Frumin, Marco Maggesi, and Niels van der Weide</em><br><!-- [et_pb_line_break_holder] --> <a href="#" class="popmake-922">Bicategories in Univalent Foundations</a></p></td><!-- [et_pb_line_break_holder] --></tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>15:30<br><!-- [et_pb_line_break_holder] --> -<br><!-- [et_pb_line_break_holder] --> 16:00</td><!-- [et_pb_line_break_holder] --> <td colspan="2">Coffee Break</td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td rowspan="4">16:00<br>-<br><!-- [et_pb_line_break_holder] --> 17:30</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #BFBFBF"><strong>FSCD Theme: Semantics</strong><br>Chair: Thierry Coquand</td><!-- [et_pb_line_break_holder] --> <td align="center" rowspan="4" style="background-color: #BAC0B1">Business Meeting</td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td style="background-color: #E3E3E3"><em>Clovis Eberhart, Tom Hirschowitz, and Alexis Laouar<br><!-- [et_pb_line_break_holder] --> </em><a href="#" class="popmake-924">Template games, simple games, and Day convolution</a></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td style="background-color: #E3E3E3"><em>Thomas Ehrhard<br><!-- [et_pb_line_break_holder] --> </em><a href="#" class="popmake-927">Differentials and distances in probabilistic coherence spaces</a></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td style="background-color: #E3E3E3"><em>Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, and Marco Maggesi<br><!-- [et_pb_line_break_holder] --> </em><a href="#" class="popmake-929">Modular specification of monads through higher-order presentations</a></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> </table>

<table style="text-align: center; border:1px"><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --><td>08:00</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #D1DBC1">Registration</td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted; "><!-- [et_pb_line_break_holder] --> <td rowspan="2" style="width: 10%">09:00<br>-<br><!-- [et_pb_line_break_holder] --> 10:00</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #D4C68D"><p><strong>FSCD Invited Talk</strong><br>Chair: Cynthia Kop</p></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td style="background-color: #EBE2BF "><h5><em>  Hongseok Yang</em></h5><!-- [et_pb_line_break_holder] --> <p><a href="#" class="popmake-643">Some semantic issues in probabilistic programming languages</a></p></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>10:00<br><!-- [et_pb_line_break_holder] --> -<br><!-- [et_pb_line_break_holder] --> 10:30</td><!-- [et_pb_line_break_holder] --> <td>Coffee Break</td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td rowspan="5">10:30<br>-<br><!-- [et_pb_line_break_holder] --> 12:30</td><!-- [et_pb_line_break_holder] --> <td colspan="2" style="background-color: #BFBFBF"><p><strong>FSCD Theme: Rewriting</strong><br>Chair: Aart Middeldorp</p></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td colspan="2" style="background-color: #E3E3E3"><em>Mirai Ikebuchi<br><!-- [et_pb_line_break_holder] --> </em><a href="#" class="popmake-931">A Lower Bound of the Number of Rewrite Rules Obtained by Homological Methods</a></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td colspan="2" style="background-color: #E3E3E3"><em>Alfons Geser, Dieter Hofbauer, and Johannes Waldmann<br><!-- [et_pb_line_break_holder] --> </em><a href="#" class="popmake-933">Sparse Tiling through Overlap Closures for Termination of String Rewriting</a></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td colspan="2" style="background-color: #E3E3E3"><em>David M. Cerna and Temur Kutsia<br><!-- [et_pb_line_break_holder] --> </em><a href="#" class="popmake-935">A generic framework for higher-order generalizations</a></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td colspan="2" style="background-color: #E3E3E3"><em>Rubén Rubio, Narciso Martí-Oliet, Isabel Pita, and Alberto Verdejo<br><!-- [et_pb_line_break_holder] --> </em><a href="#" class="popmake-937">Model checking strategy-controlled rewriting systems <br><!-- [et_pb_line_break_holder] --> (System Description)</a></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>12:30<br><!-- [et_pb_line_break_holder] --> -<br><!-- [et_pb_line_break_holder] --> 14:00</td><!-- [et_pb_line_break_holder] --> <td>Lunch Break</td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --><tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td rowspan="3">14:00<br>-<br><!-- [et_pb_line_break_holder] --> 15:00</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #BFBFBF"><strong>FSCD Theme: Rewriting and Types</strong><Br>Chair: Johannes Waldmann</td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --><tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td style="background-color: #E3E3E3"><p><em>Łukasz Czajka and Cynthia Kop</em><br><!-- [et_pb_line_break_holder] --> <a href="#" class="popmake-939">Polymorphic Higher-order Termination</a></p></td><!-- [et_pb_line_break_holder] --></tr><!-- [et_pb_line_break_holder] --><tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td style="background-color: #E3E3E3"><p><em>Frédéric Blanqui, Guillaume Genestier and Olivier Hermant<br><!-- [et_pb_line_break_holder] --> </em><a href="#" class="popmake-941">Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting</a></p></td><!-- [et_pb_line_break_holder] --></tr><!-- [et_pb_line_break_holder] --><tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>15:00<br><!-- [et_pb_line_break_holder] --> -<br><!-- [et_pb_line_break_holder] --> 15:30</td><!-- [et_pb_line_break_holder] --> <td><strong>Group Photo</strong></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>17:00<br>-<br><!-- [et_pb_line_break_holder] --> 22:30</td><!-- [et_pb_line_break_holder] --> <td colspan="2" style="background-color: #D1C5DC"><strong>Excursion & Banquet</strong></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> </table>

<table style="text-align: center; border:1px"><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <TD width="10%"></TD><!-- [et_pb_line_break_holder] --> <td width="30%"><strong>Main Conference </strong></td><!-- [et_pb_line_break_holder] --> <td width="33%"><strong>IWC 2019 / HOR 2019</strong></td><!-- [et_pb_line_break_holder] --><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --><td>08:00</td><!-- [et_pb_line_break_holder] --> <td colspan="2" style="background-color: #D1DBC1">Registration</td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted; "><!-- [et_pb_line_break_holder] --> <td rowspan="2" style="width: 10%">09:00<br>-<br><!-- [et_pb_line_break_holder] --> 10:00</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #D4C68D"><p><strong>FSCD Invited Talk</strong><br>Chair: Temur Kutsia</p></td><!-- [et_pb_line_break_holder] --> <TD style="background-color: #d7bde2 ">Session 1<br><strong>Chair: </strong>Mauricio Ayala-Rincón<!-- [et_pb_line_break_holder] --> <h4>09:00 - 09:15</h4> Welcome<!-- [et_pb_line_break_holder] --> </TD><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td style="background-color: #EBE2BF "><h5><em>Sarah Winkler</em></h5><!-- [et_pb_line_break_holder] --> <p><a href="#" class="popmake-626">Extending Maximal Completion</a></p></td><!-- [et_pb_line_break_holder] --> <td style="background-color: #ebdef0 "><Strong>Invited Talk: </Strong>Higher-order Termination<br><i>Cynthia Kop</i></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>10:00<br><!-- [et_pb_line_break_holder] --> -<br><!-- [et_pb_line_break_holder] --> 10:30</td><!-- [et_pb_line_break_holder] --> <td colspan="3">Coffee Break</td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td rowspan="2">10:30<br>-<br><!-- [et_pb_line_break_holder] --> 11:00</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #BFBFBF"><p><strong>FSCD Theme: Rewriting</strong><Br>Chair: Delia Kesner</p></td><!-- [et_pb_line_break_holder] --> <td STYLE="background-color: #d7bde2">Session 2 <br><strong>Chair: </strong>Stefano Guerrini</td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td style="background-color: #E3E3E3"><em>Claudia Faggian<br><!-- [et_pb_line_break_holder] --> </em><a href="#" class="popmake-943">Probabilistic Rewriting: Normalization, Termination, and Unique Normal Forms</a></td><!-- [et_pb_line_break_holder] --> <td style="background-color: #f2d7d5 "> RP IWC: Proving Non-Joinability using Weakly Monotone Algebras <br><i>Bertram Felgenhauer and Johannes Waldmann</i></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --><tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td rowspan="4">11:00<br>-<br><!-- [et_pb_line_break_holder] --> 12:30</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #BFBFBF"><strong>FSCD Theme: Linear Logic</strong><br>Chair: Stefano Guerrini </td><!-- [et_pb_line_break_holder] --> <td style="background-color: #f2d7d5"><h4>11:00 - 11:30</h4>RP IWC: The Diamond Lemma for non-terminating rewriting systems using deterministic reduction strategies<br><i>Cyrille Chenavier and Maxime Lucas</i></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --><tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td style="background-color: #E3E3E3"><p><em>Ross Horne<br><!-- [et_pb_line_break_holder] --> </em><a href="#" class="popmake-945">The Sub-Additives: A Proof Theory for Probabilistic Choice extending Linear Logic</a></p></td><!-- [et_pb_line_break_holder] --> <td style="background-color: #f2d7d5"><h4>11:30 - 12:00</h4>RP IWC: infChecker, a tool for checking infeasibility<br><i> Raúl Gutiérrez and Salvador Lucas</i></td><!-- [et_pb_line_break_holder] --></tr><!-- [et_pb_line_break_holder] --><tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td style="background-color: #E3E3E3"><em>Yosuke Fukuda and Akira Yoshimizu<br><!-- [et_pb_line_break_holder] --> </em><a href="#" class="popmake-947">A Linear-logical Reconstruction of Intuitionistic Modal Logic S4</a></td><!-- [et_pb_line_break_holder] --> <td rowspan="2" style="background-color: #d0ece7 "><H4>12:00 - 12:30</H4> RP HOR: SizeChangeTool: A Termination Checker for Higher-Order Rewriting with Dependent Types<BR><I>Guillaume Genestier</I></td><!-- [et_pb_line_break_holder] --></tr><!-- [et_pb_line_break_holder] --><tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td style="background-color: #E3E3E3"><p><em>Willem B. Heijltjes, Dominic J. D. Hughes, and Lutz Straßburger</em><br><!-- [et_pb_line_break_holder] --> <a href="#" class="popmake-949">Proof nets for first-order additive linear logic</a></p></td><!-- [et_pb_line_break_holder] --></tr><!-- [et_pb_line_break_holder] --><tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --><td>12:30<br><!-- [et_pb_line_break_holder] --> -<br><!-- [et_pb_line_break_holder] --> 14:00</td><!-- [et_pb_line_break_holder] --> <td colspan="2">Lunch Break</td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --><tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --><td rowspan="2">14:00<br><!-- [et_pb_line_break_holder] --> -<br><!-- [et_pb_line_break_holder] --> 14:45</td><!-- [et_pb_line_break_holder] --> <td rowspan="3" style="background-color: #BAC0B1"><strong>FSCD General Meeting</strong></td><!-- [et_pb_line_break_holder] --> <td STYLE="background-color: #d7bde2">Session 3<br><strong>Chair: </strong>Silvia Ghilezan</td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td style="background-color: #ebdef0 "><strong>Invited Talk: </strong>Higher-Order Complexity Analysis With First-Order Tools <br><i>Martin Avanzini</i></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>14:45 - 15:30</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #ebdef0 "><strong>Invited Talk: </strong>On the Ground Confluence of Order-sorted Conditional Specifications Modulo Axioms: Maude's Church-Rosser Checker<br><i> Francisco Durán</i></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>15:30 - 16:00</td><!-- [et_pb_line_break_holder] --> <td></td><!-- [et_pb_line_break_holder] --> <td>Coffee Break</td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr><!-- [et_pb_line_break_holder] --> <td rowspan="2">16:00 - 16:45</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #fcf3cf "></td><!-- [et_pb_line_break_holder] --> <td STYLE="background-color: #d7bde2">Session 4 <br><strong>Chair: </strong>Jakob Grue Simonsen</td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> <td style="background-color: #fcf3cf "></td><!-- [et_pb_line_break_holder] --> <td style="background-color: #ebdef0 "><strong>Invited Talk: </strong>On the Clocked Lambda-Calculus<br><i> Jörg Endrullis</i></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr><!-- [et_pb_line_break_holder] --> <td>16:45 - 17:30</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #fcf3cf "></td><!-- [et_pb_line_break_holder] --> <td style="background-color: #ebdef0 "><strong>Invited Talk: </strong>Degrees of extensionality in the theory of Böhm trees<br><i>Giulio Manzonetto</i></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr><!-- [et_pb_line_break_holder] --> <td>17:30 - 18:00</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #fcf3cf "></td><!-- [et_pb_line_break_holder] --> <td style="background-color: #f2d7d5">RP IWC: Residuals Revisited<br><i>Christina Kohl and Aart Middeldorp</i></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr><!-- [et_pb_line_break_holder] --> <td>18:00-18:30</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #fcf3cf "></td><!-- [et_pb_line_break_holder] --> <td style="background-color: #ebdef0 ">CoCo report<br><i>Aart Middeldorp</i></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> </table><!-- [et_pb_line_break_holder] -->

<h2><CENTER>Saturday 29 June, 2019</CENTER></h2><!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> <table style="text-align: center; border:1px"><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td width="10%"></td><!-- [et_pb_line_break_holder] --> <td width="44%"><strong>TLLA 2019</strong></td><!-- [et_pb_line_break_holder] --> <td width="46%"><strong>SD 2019</strong></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --><td>08:00 </td><!-- [et_pb_line_break_holder] --> <td colspan="2" style="background-color: #D1DBC1">Registration </td><!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td style="width: 10%">09:00 - 10:00</td><!-- [et_pb_line_break_holder] --> <td colspan="2" style="background-color: #d5dbdb"><strong>Joint invited talk: </strong> Reasoning about languages with control operators<!-- [et_pb_line_break_holder] --> <BR><!-- [et_pb_line_break_holder] --> <i>Delia Kesner</i><!-- [et_pb_line_break_holder] --> </td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>10:00 - 10:30</td><!-- [et_pb_line_break_holder] --> <td colspan="2" style="background-color: #f8d9d3">Coffee Break</td><!-- [et_pb_line_break_holder] --> </tr> <!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>10:30 - 11:00</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #eaeded ">Proof nets for non-wellfounded proofs<br><i>Abhishek De and Alexis Saurin</i></td><!-- [et_pb_line_break_holder] --> <td rowspan="2" style="background-color: #d5dbdb "><strong>Invited Talk:</strong> Can we Prove Privacy Properties using the Calculus of Structures<!-- [et_pb_line_break_holder] --> <BR><!-- [et_pb_line_break_holder] --> <i>Ross Horne</i></td><!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>11:00 - 11:30</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #eaeded ">A Quantitative Semantics of Differential Linear Logic with Setoids<br><!-- [et_pb_line_break_holder] --> <i>Zeinab Galal</i></td><!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>11:30 - 12:00</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #eaeded"></td><!-- [et_pb_line_break_holder] --> <td style="background-color: #eaeded " >Deep inference for proof search<br><i>Ozan Kahramanogullari</i></td><!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>12:00 - 12:30</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #eaeded"></td><!-- [et_pb_line_break_holder] --> <td style="background-color: #eaeded">Additive to Classical Proof Search<br><i>Adam Lassiter</i></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>12:30 - 14:00</td><!-- [et_pb_line_break_holder] --> <td colspan="2" style="background-color: #f8d9d3">Lunch Break</td><!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td >14:00 - 15:00</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #d5dbdb"><strong>Invited Talk: </strong>Call-by-push-value and linear logic: various connections<br><i>Paul Blain Levy</i></td><!-- [et_pb_line_break_holder] --> <td style="background-color: #d5dbdb "><strong>Invited Talk: </strong>Deciding ATL* satisfiability by tableaux<br><i>Serenella Cerrito</i></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>15:00 - 15:30</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #eaeded ">On the expressivity of linear recursion schemes<br><i>Pierre Clairambault and Andrzej Murawski</i></td><!-- [et_pb_line_break_holder] --> <td style="background-color: #eaeded">Two deductive systems for the constructive logic S4, a formal verification<br><i>Lourdes Del Carmen González Huesca</i></td><!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>15:30 - 16:00</td><!-- [et_pb_line_break_holder] --> <td colspan="2" style="background-color: #f8d9d3">Coffee Break</td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>16:00 - 16:30</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #eaeded"> </td><!-- [et_pb_line_break_holder] --> <td style="background-color: #eaeded">What are combinatorial proofs? <br><i>Lutz Strassburger</i></td><!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> <TR style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <TD>16:30 - 17:00</TD><!-- [et_pb_line_break_holder] --> <td rowspan="2" style="background-color: #FCF3CF">Business Meeting</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #eaeded ">Expansion tree proofs with unification<br><i>Michelangelo Mecozzi</i></td><!-- [et_pb_line_break_holder] --> </TR><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td >17:00 - 17:30</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #eaeded ">The Jacobson Radical of a Propositional Theory<br><i>Peter Schuster</i></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> </table>

<h2><CENTER>Sunday 30 June, 2019</CENTER></h2><!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> <table style="text-align: center; border:1px"><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td width="10%"></td><!-- [et_pb_line_break_holder] --> <td width="44%"><strong>TLLA 2019</strong></td><!-- [et_pb_line_break_holder] --> <td width="46%"><strong>SD 2019</strong></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --><td>08:00 </td><!-- [et_pb_line_break_holder] --> <td colspan="2" style="background-color: #D1DBC1">Registration </td><!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td style="width: 10%">09:00 - 10:00</td><!-- [et_pb_line_break_holder] --> <td colspan="2" style="background-color: #d5dbdb"><strong>Joint Invited Talk:</strong> Semantics and complexity lower bounds<!-- [et_pb_line_break_holder] --> <BR><!-- [et_pb_line_break_holder] --> <i>Thomas Seiller</i><!-- [et_pb_line_break_holder] --> </td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>10:00 - 10:30</td><!-- [et_pb_line_break_holder] --> <td colspan="2" style="background-color: #f8d9d3">Coffee Break</td><!-- [et_pb_line_break_holder] --> </tr> <!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>10:30 - 11:00</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #eaeded ">About the Power of Taylor Expansion<!-- [et_pb_line_break_holder] --> <br><i>Davide Barbarossa and Giulio Manzonetto</i></td><!-- [et_pb_line_break_holder] --> <td rowspan="2" style="background-color: #d5dbdb "><strong>Invited Talk:</strong> A story of multiplicatives and additives<!-- [et_pb_line_break_holder] --> <BR><!-- [et_pb_line_break_holder] --> <i>Andrea Aler Tubella</i></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>11:00 - 11:30</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #eaeded ">What is the Taylor expansion a natural transformation of?<br><i>Luc Pellissier</i></td><!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>11:30 - 12:00</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #eaeded ">Standardization via Linear Logic for Call-by-Name, Call-by-Value and Choice Effects<br><!-- [et_pb_line_break_holder] --> <i>Claudia Faggian and Giulio Guerrieri</i></td><!-- [et_pb_line_break_holder] --> <td style="background-color: #eaeded " >A Subatomic Proof System for Binary Decision Trees<br><i> Chris Barrett</i></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>12:00 - 12:30</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #eaeded">The Geometry of Abstract Machines <br><i>Beniamino Accattoli, Ugo Dal Lago and Gabriele Vanoni</i></td><!-- [et_pb_line_break_holder] --> <td style="background-color: #eaeded"> A graph theoretic extension of Boolean logic<br><i>Tim Waring</i></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>12:30 - 14:00</td><!-- [et_pb_line_break_holder] --> <td colspan="2" style="background-color: #f8d9d3">Lunch Break</td><!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td >14:00 - 15:00</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #d5dbdb"><strong>Invited Talk: </strong>Stable Semantics of Probabilistic Higher-Order Programs<br><i>Raphaëlle Crubillé. </i></td><!-- [et_pb_line_break_holder] --> <td style="background-color: #d5dbdb "><strong>Invited Talk: </strong>Structural proof theory: shedding structure<br><i>Revantha Ramanayake</i></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>15:00 - 15:30</td><!-- [et_pb_line_break_holder] --> <td style="background-color:#eaeded">Transductions in affine logic<br><i>Lê Thành Dung Nguyen</i></td><!-- [et_pb_line_break_holder] --> <td style="background-color: #eaeded">Complexity of Reasoning in Residuated Kleene Algebras<br><i>Stepan Kuznetsov</i></td><!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>15:30 - 16:00</td><!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> <td colspan="2"style="background-color: #f8d9d3">Coffee Break</td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td>16:00 - 16:30</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #eaeded"></td><!-- [et_pb_line_break_holder] --> <td style="background-color: #eaeded">The Spinal Atomic Lambda Calculus <br><i>David Sherratt</i></td><!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> <TR style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <TD>16:30 - 17:00</TD><!-- [et_pb_line_break_holder] --> <td rowspan="2" style="background-color: #eaeded"></td><!-- [et_pb_line_break_holder] --> <td style="background-color: #eaeded ">Kreisel's Conjecture and Reflexion Principles: Two Restricted Versions of the Conjecture<br><i>Paulo Guiherme Santos</i></td><!-- [et_pb_line_break_holder] --> </TR><!-- [et_pb_line_break_holder] --> <tr style="border-top: 2px; border-top-style: dotted"><!-- [et_pb_line_break_holder] --> <td >17:00 - 17:30</td><!-- [et_pb_line_break_holder] --> <td style="background-color: #eaeded ">On sequent calculi proofs in relevant logics<br><i>Mirjana Ilic</i></td><!-- [et_pb_line_break_holder] --> </tr><!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] --> </table><!-- [et_pb_line_break_holder] --> <!-- [et_pb_line_break_holder] -->