Registered participants at the conference can find the program with links to preprints here. A password will be\ distributed at the conference.
Monday 24th June 2019 - Tuesday 25th June 2019 - Wednesday 26th June 2019 - Thursday 27th 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 |
Higher-order 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 Higher-order Logic Modulo Theories. C.-H. Luke Ong and Dominik Wagner |
|
Canonisation and Definability for Graphs of Bounded Rank Width.. Martin Grohe and Daniel Neuen |
LambdaY-calculus with priorities. Igor Walukiewicz |
|
Walk refinement, walk logic, and the iteration number of the Weisfeiler-Leman 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 First-Order 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. Goubault-Larrecq |
Type-Based Complexity Analysis of Probabilistic Functional Programs. Martin Avanzini, Alexis Ghyselen and Ugo Dal Lago |
Template games and differential linear logic. Paul-André Melliès |
|
Lambda Calculus and Probabilistic Computation - A foundational approach. Claudia Faggian and Simona Ronchi Della Rocca |
High-level methods for homotopy construction in associative n-categories. David Reutter and Jamie Vicary |
|
On the Termination Problem for Probabilistic Higher-Order 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 First-Order Grammars is ACKERMANN-Complete. Petr Jančar and Sylvain Schmitz |
Differentiable Causal Computations via Delayed Trace. David Sprunger and Shin-Ya Katsumata |
|
On the Existential Theories of Büchi Arithmetic and Linear p-adic Fields. Florent Guépin, Christoph Haase and James Worrell |
A Sequent Calculus for Opetopes. Pierre-Louis 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 Number-theoretic 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 Ontology-Mediated 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 Primitive-Recursive 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, Shin-Ya Katsumata, Nick Hu, Bartek Klin and Ichiro Hasuo |
Why propositional quantification makes modal logics on trees robustly hard ? Bartosz Bednarczyk and Stéphane Demri |
|
No-Go 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 |
Point-width and Max-CSPs. Clément Carbonnel, Miguel Romero and Stanislav Živný |
|
A Probabilistic and Non-Deterministic Call-by-Push-Value Language. Jean Goubault-Larrecq |
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 |
|
Higher-Kinded 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 Near-Optimal Axiomatisation of ZX-Calculus for Pure Qubit Quantum Mechanics. Renaud Vilmart |
|
Long-run satisfaction of path properties. Christel Baier, Nathalie Bertrand, Jakob Piribauer and Ocan Sankur |
A Generic Normal Form for ZX-Diagrams 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íaz-Caro, 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 Shin-Ya 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 Shin-Ya Katsumata |
|
4pm - 5pm |
Modal logics Chair: H. H. Hansen |
Category theory Chair:
U. Dal Lago |
History-dependent nominal mu-calculus. Bartek Klin and Clovis Eberhart |
Graphical Affine Algebra. Filippo Bonchi, Robin Piedeleu, Pawel Sobocinski and Fabio Zanasi |
|
Matching mu-Logic. Xiaohong Chen and Grigore Rosu |
The convex hull of finitely generable subsets and its predicate transformer. Mohammad Javad Davari, Abbas Edalat and Andre Lieutier |