| Authors | Title | Paper | Talk |
|---|
| Nicola Gambino | A unified approach to Univalent Foundations and Homotopical Algebra |  | |
| Kohei Honda, Nobuko Yoshida and Martin Berger | Process Types as a Descriptive Tool for Interaction: Control and the Pi-Calculus |  | |
| Manfred Schmidt-Schauss | Concurrent Programming Languages and Methods for Semantic Analyses (Extended Abstract of Invited Talk) |  | |
| Andreas Abel, Brigitte Pientka, Anton Setzer and David Thibodeau | Unnesting of Copatterns |  | Jul 15 17:30 |
| Takahito Aoto, Yoshihito Toyama and Kazumasa Uchida | Proving Confluence of Term Rewriting Systems via Persistency and Decreasing Diagrams |  | Jul 14 17:30 |
| Kyungmin Bae and Jose Meseguer | Predicate Abstraction of Rewrite Theories |  | Jul 16 11:15 |
| Marc Bagnol and Clément Aubert | Unification and Logarithmic Space |  | Jul 14 11:45 |
| Stefano Berardi and Silvia Steila | Ramsey Theorem as an intuitionistic property of well founded relations |  | Jul 15 10:45 |
| Aleš Bizjak, Lars Birkedal and Marino Miculan | A Model of Countable Nondeterminism in Guarded Type Theory |  | Jul 16 15:30 |
| Guillaume Burel | Cut Admissibility by Saturation |  | Jul 16 10:45 |
| Carles Creus and Guillem Godoy | Automatic Evaluation of Context-Free Grammars (System Description) |  | Jul 14 12:45 |
| Carles Creus and Guillem Godoy | Tree Automata with Height Constraints between Brothers |  | Jul 17 10:45 |
| Łukasz Czajka | A Coinductive Confluence Proof for Infinitary Lambda-Calculus. |  | Jul 14 16:30 |
| Daniel de Carvalho and Jakob Grue Simonsen | An Implicit Characterization of the Polynomial-Time Decidable Sets by Cons-Free Rewriting |  | Jul 14 11:15 |
| Mariangiola Dezani-Ciancaglini and Silvia Ghilezan | Preciseness of subtyping on intersection and union types |  | Jul 16 17:30 |
| Martin Escardo and Alex Simpson | Abstract datatypes for real numbers in type theory |  | Jul 16 16:30 |
| Peng Fu and Aaron Stump | Self Types for Dependently Typed Lambda Encodings |  | Jul 15 16:30 |
| Carsten Fuhs and Cynthia Kop | First-Order Formative Rules |  | Jul 15 11:45 |
| Nao Hirokawa and Georg Moser | Automated Complexity Analysis Based on Context-Sensitive Rewriting |  | Jul 14 12:15 |
| Martin Hofmann and Georg Moser | Amortised Resource Analysis and Typed Polynomial Interpretations |  | Jul 15 15:30 |
| Jiaxiang Liu, Nachum Dershowitz and Jean-Pierre Jouannaud | Confluence by Critical Pair Analysis |  | Jul 14 17:00 |
| Carlos Lombardi, Alejandro Rios and Roel de Vrijer | Proof terms for infinitary rewriting |  | Jul 17 11:45 |
| Roberto Maieli | Construction of retractile proof structures |  | Jul 16 12:15 |
| Paul-André Melliès | Local states in string diagrams |  | Jul 16 17:00 |
| Koji Nakazawa and Tomoharu Nagai | Reduction System for Extensional Lambda-mu Calculus |  | Jul 17 11:15 |
| Cody Roux and Floris van Doorn | The Structural Theory of Pure Type Systems |  | Jul 15 17:00 |
| Manfred Schmidt-Schauss and David Sabel | Applicative May- and Should-Simulation in the Call-by-Value Lambda Calculus with AMB |  | Jul 14 15:30 |
| Sylvain Schmitz | Implicational Relevance Logic is 2-ExpTime-Complete |  | Jul 14 10:45 |
| Richard Statman | Near semi-rings and lambda calculus |  | Jul 17 12:15 |
| Andrei Stefanescu, Stefan Ciobaca, Radu Mereuta, Brandon Moore, Traian Florin Serbanuta and Grigore Rosu | All-Path Reachability Logic |  | Jul 16 11:45 |
| Christian Sternagel and René Thiemann | Formalizing monotone algebras for certification of termination- and complexity proofs |  | Jul 15 12:15 |
| Thomas Sternagel and Aart Middeldorp | Conditional Confluence (System Description) |  | Jul 14 18:00 |
| Akihisa Yamada, Keiichirou Kusakari and Toshiki Sakabe | Nagoya Termination Tool |  | Jul 15 12:45 |
| Hans Zantema, Barbara Koenig and Sander Bruggink | Termination of Cycle Rewriting |  | Jul 15 11:15 |