| Authors | Title | Paper | Talk |
|---|
| Stéphanie Delaune | Analysing privacy-type properties in cryptographic protocols |  | |
| Grigore Rosu | Formal Design, Implementation and Verification of Blockchain Languages | | |
| Peter Selinger | Challenges in quantum programming languages | | |
| Valeria Vignudelli | Proof techniques for program equivalence in probabilistic higher-order languages | | |
| Sandra Alves and Sabine Broda | A Unifying Framework for Type Inhabitation | | Jul 10 11:00 |
| Nirina Andrianarivelo and Pierre Rety | Confluence of Prefix-Constrained Rewrite Systems | | Jul 12 17:00 |
| Mauricio Ayala-Rincon, Maribel Fernandez and Daniele Nantes-Sobrinho | Fixed-Point Constraints for Nominal Equational Unification | | Jul 12 11:00 |
| Patrick Bahr | Strict Ideal Completions of the Lambda Calculus | | Jul 11 10:00 |
| Alexander Baumgartner, Temur Kutsia, Jordi Levy and Mateu Villaret | Term-Graph Anti-Unification | | Jul 12 10:00 |
| Willem Heijltjes and Gianluigi Bellin | Proof nets for bi-intuitionistic linear logic | | Jul 09 11:00 |
| Maciej Bendkowski and Pierre Lescanne | Counting Environments and Closures | | Jul 10 15:40 |
| David Cerna and Temur Kutsia | Higher-Order Equational Pattern Anti-Unification | | Jul 12 11:30 |
| Łukasz Czajka | Term rewriting characterisation of LOGSPACE for finite and infinite data | | Jul 10 16:10 |
| Joerg Endrullis, Jan Willem Klop and Roy Overbeek | Decreasing diagrams with two labels are complete for confluence of countable systems | | Jul 12 16:30 |
| Simon Forest and Samuel Mimram | Coherence of Gray categories via rewriting | | Jul 12 17:30 |
| Thomas Genet | Completeness of Tree Automata Completion | | Jul 11 12:00 |
| Amar Hadzihasanovic, Giovanni de Felice and Kang Feng Ng | A diagrammatic axiomatisation of fermionic quantum circuits | | Jul 09 15:00 |
| Mirai Ikebuchi and Keisuke Nakano | On repetitive right application of B-terms | | Jul 11 09:00 |
| Rohan Jacob-Rao, Brigitte Pientka and David Thibodeau | Index-Stratified Types | | Jul 10 12:00 |
| Ambrus Kaposi and András Kovács | A Syntax for Higher Inductive-Inductive Types | | Jul 10 15:00 |
| Jean-Simon Lemay | Lifting Coalgebra Modalities and IMELL Model Structure to Eilenberg-Moore Categories | | Jul 09 12:00 |
| Daniel R. Licata, Ian Orton, Andrew M. Pitts and Bas Spitters | Internal Universes in Models of Homotopy Type Theory | | Jul 10 10:00 |
| Bassel Mannaa and Rasmus Møgelberg | The clocks they are adjunctions. Denotational semantics for Clocked Type Theory | | Jul 10 09:30 |
| Max New and Daniel Licata | Call-by-name Gradual Type Theory | | Jul 10 09:00 |
| Lê Thành Dũng Nguyễn | Unique perfect matchings and proof nets | | Jul 09 11:30 |
| Naoki Nishida and Yuya Maeda | Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems | | Jul 11 11:00 |
| Paweł Parys | Homogeneity without Loss of Generality | | Jul 11 09:30 |
| Manfred Schmidt-Schauss and David Sabel | Nominal Unification with Atom and Context Variables | | Jul 12 12:00 |
| Amin Timany and Matthieu Sozeau | Cumulative Inductive Types in Coq | | Jul 10 11:30 |
| Sarah Winkler and Aart Middeldorp | Completion for Logically Constrained Rewriting | | Jul 11 11:30 |
| Christina Kohl and Aart Middeldorp | ProTeM: A Proof Term Manipulator | | Jul 12 15:00 |
| Takahito Aoto, Makoto Hamana, Nao Hirokawa, Aart Middeldorp, Julian Nagele, Naoki Nishida, Kiraku Shintani and Harald Zankl | Confluence Competition 2018 | | |