Registered participants at the conference can find the program with links to preprints here. A password will be\ distributed at the conference.
Monday 24^{th} June 2019  Tuesday 25^{th} June 2019  Wednesday 26^{th} June 2019  Thursday 27^{th} June 20198am  9am  Coffee and pastries  

9am  10am 
Invited talk: Nicole Schweikardt
Local normal forms and their use in algorithmic meta theorems Chair: P. Bouyer 

10:30am  12:30am 
Finite model theory & Counting logic
Chair: N. Schweikardt 
Higherorder logic & Proof theory Chair: D. Miller 
On the Power of Symmetric Linear Programs. Albert Atserias, Anuj Dawar and Joanna Ochremiak 
HoCHC: A Refutationally Complete and Semantically Invariant System of Higherorder Logic Modulo Theories. C.H. Luke Ong and Dominik Wagner 

Canonisation and Definability for Graphs of Bounded Rank Width.. Martin Grohe and Daniel Neuen 
LambdaYcalculus with priorities. Igor Walukiewicz 

Walk refinement, walk logic, and the iteration number of the WeisfeilerLeman algorithm. Moritz Lichter, Ilia Ponomarenko and Pascal Schweitzer 
A Type Theory for Defining Logics and Proofs. Brigitte Pientka, David Thibodeau, Andreas Abel, Francisco Ferreira and Rebecca Zucchini 

Learning Concepts Definable in FirstOrder Logic with Counting. Steffen van Bergerem 
Intuitionistic Proofs Without Syntax. Willem Heijltjes, Dominic Hughes and Lutz Straßburger 

2pm  3:30pm 
Probabilistic programming Chair:
B. Pientka 
Homotopy theory Chair:
J. GoubaultLarrecq 
TypeBased Complexity Analysis of Probabilistic Functional Programs. Martin Avanzini, Alexis Ghyselen and Ugo Dal Lago 
Template games and differential linear logic. PaulAndré Melliès 

Lambda Calculus and Probabilistic Computation  A foundational approach. Claudia Faggian and Simona Ronchi Della Rocca 
Highlevel methods for homotopy construction in associative ncategories. David Reutter and Jamie Vicary 

On the Termination Problem for Probabilistic HigherOrder Recursive Programs. Naoki Kobayashi, Ugo Dal Lago and Charles Grellois 
Path Spaces of Higher Inductive Types in Homotopy Type Theory. Nicolai Kraus and Jakob von Raumer 

4pm  5pm 
Verification Chair: S. Akshay 
Category theory Chair: P.A. Melliès 
Bisimulation Equivalence of FirstOrder Grammars is ACKERMANNComplete. Petr Jančar and Sylvain Schmitz 
Differentiable Causal Computations via Delayed Trace. David Sprunger and ShinYa Katsumata 

On the Existential Theories of Büchi Arithmetic and Linear padic Fields. Florent Guépin, Christoph Haase and James Worrell 
A Sequent Calculus for Opetopes. PierreLouis Curien, Cédric Ho Thanh and Samuel Mimram 

6pm 
Reception in Djavad Mowafaghian World Art Centre, Room G 2555 in SFU Goldcorp building 
8am  9am  Coffee and pastries  

9am  10am 
Invited talk: Peter Selinger Numbertheoretic methods in quantum computing Chair: S. Abramsky 

10:30am  12pm 
Quantum computing
Chair: P. Selinger 
Description and Horn logics
Chair: A. Dawar 
Quantum channels as a categorical completion. Mathieu Huot and Sam Staton 
Model Comparison Games for Horn Description Logics. Jean Christoph Jung, Fabio Papacchini, Frank Wolter and Michael Zakharyaschev 

Categorical Semantics for Time Travel. Nicola Pinzani, Stefano Gogioso and Bob Coecke 
When is OntologyMediated Querying Efficient? Pablo Barceló, Cristina Feier, Carsten Lutz and Andreas Pieris 

A comonadic view of simulation and quantum resources. Samson Abramsky, Rui Soares Barbosa, Martti Karvonen and Shane Mansfield 
Descriptive complexity for minimal time of cellular automata. Étienne Grandjean and Théo Grente 

1:30pm  3:30pm  Invited tutorial: Andrei Bulatov A short story of the CSP dichotomy conjecture Chair: D. Miller 

4pm  5pm 
Category theory Chair: S.Y. Katsumata 
Verification
Chair: J. Worrell 
Describing free ωcategories. Simon Forest and Samuel Mimram 
Reachability in Vector Addition Systems is PrimitiveRecursive in Fixed Dimension. Jérôme Leroux and Sylvain Schmitz 

Backprop as Functor: A compositional perspective on supervised learning. Brendan Fong, David I. Spivak and Remy Tuyeras 
Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests. Christoph Haase and Georg Zetzsche 
8am  9am  Coffee and pastries  

9am  11am 
Invited tutorial: Daniela Petrisan A categorical approach to automata theory Chair: A. Pitts 

11:30am  12:30pm 
Category theory
Chair: A. Polonsky 
Modal and temporal logics
Chair: I. Walukiewicz 
Codensity Games for Bisimilarity. Yuichi Komorida, ShinYa Katsumata, Nick Hu, Bartek Klin and Ichiro Hasuo 
Why propositional quantification makes modal logics on trees robustly hard ? Bartosz Bednarczyk and Stéphane Demri 

NoGo Theorems for Distributive Laws. Maaike Zwart and Dan Marsden 
The Hierarchy of Hyperlogics. Norine Coenen, Bernd Finkbeiner, Christopher Hahn and Jana Hofmann 

2pm  3:30pm 
Probabilistic
programming
Chair: P. Panangaden 
Constraint
satisfaction problems
Chair: A. Bulatov 
The Theory of Traces for Systems with Probability and Nondeterminism. Filippo Bonchi, Ana Sokolova and Valeria Vignudelli 
Pointwidth and MaxCSPs. Clément Carbonnel, Miguel Romero and Stanislav Živný 

A Probabilistic and NonDeterministic CallbyPushValue Language. Jean GoubaultLarrecq 
Promises Make Finite (Constraint Satisfaction) Problems Infinitary. Libor Barto 

The Geometry of Bayesian Programming. Ugo Dal Lago and Naohiko Hoshino 
Topology is relevant (in the infinite domain dichotomy conjecture for constraint satisfaction problems). Manuel Bodirsky, Antoine Mottet, Miroslav Olšák, Jakub Opršal, Michael Pinsker and Ross Willard 

4pm  5pm 
Type theory Chair:
N. Kobayashi 
Dynamic logic
and applications
Chair: M. Randour 
A type theory for cartesian closed bicategories. Marcelo Fiore and Philip Saville 
Timed systems through the lens of logic. S. Akshay, Paul Gastin, Vincent Jugé and Krishna S 

HigherKinded Data Types: Syntax and Semantics. Patricia Johann and Andrew Polonsky 
Completeness for Game Logic. Sebastian Enqvist, Helle Hvid Hansen, Clemens Kupke, Johannes Marti and Yde Venema 

5pm  7pm 
Award ceremony + business meeting
Room B 

7:30pm 10:00pm  Conference dinner in Top of Vancouver revolving restaurant 
8am  9am  Coffee and pastries  

9am  10am 
Invited talk: James Worrell
Orbit Problems for Linear Dynamical Systems Chair: S. Schmitz 

10:30am  12:30pm 
Quantitative verification & Games
Chair: C. Haase 
Quantum computing Chair: J. Vicary 
Perspective Games. Orna Kupferman and Gal Vardi 
A NearOptimal Axiomatisation of ZXCalculus for Pure Qubit Quantum Mechanics. Renaud Vilmart 

Longrun satisfaction of path properties. Christel Baier, Nathalie Bertrand, Jakob Piribauer and Ocan Sankur 
A Generic Normal Form for ZXDiagrams and Application to the Rational Angle Completeness. Emmanuel Jeandel, Simon Perdrix and Renaud Vilmart 

MSO+nabla is undecidable. Mikołaj Bojańczyk, Edon Kelmendi and Michał Skrzypczak 
Realizability in the Unitary Sphere. Alejandro DíazCaro, Mauricio Guillermo, Alexandre Miquel and Benoît Valiron 

Graph Planning with Expected Finite Horizon. Krishnendu Chatterjee and Laurent Doyen 
Quantum Hoare Logic with Ghost Variables. Dominique Unruh 

2pm  3:30pm 
Automata theory
& Algebra Chair:
D. Petrisan 
Probabilistic
reasoning & Security Chair:
P. Panangaden 
The logic of action lattices is undecidable. Stepan Kuznetsov 
Probabilistic Relational Reasoning via Metrics. Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu and ShinYa Katsumata 

Block products for algebras over countable words and applications to logic. Bharat Adsul, Saptarshi Sarkar and A. V. Sreejith 
Algorithmic barriers to representing conditional independence. Nathanael Ackerman, Jeremy Avigad, Cameron Freer, Daniel Roy and Jason Rute 

Separation and covering for group based concatenation hierarchies. Thomas Place and Marc Zeitoun 
Approximate Span Liftings: Compositional Semantics for Relaxations of Differential Privacy. Tetsuya Sato, Gilles Barthe, Marco Gaboardi, Justin Hsu and ShinYa Katsumata 

4pm  5pm 
Modal logics Chair: H. H. Hansen 
Category theory Chair:
U. Dal Lago 
Historydependent nominal mucalculus. Bartek Klin and Clovis Eberhart 
Graphical Affine Algebra. Filippo Bonchi, Robin Piedeleu, Pawel Sobocinski and Fabio Zanasi 

Matching muLogic. Xiaohong Chen and Grigore Rosu 
The convex hull of finitely generable subsets and its predicate transformer. Mohammad Javad Davari, Abbas Edalat and Andre Lieutier 