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 | | |