Program of LICS 2019

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 2019

Room information

Monday 24th June 2019

8am - 9am Coffee and pastries
9am - 10am Invited talk: Nicole Schweikardt
Local normal forms and their use in algorithmic meta theorems

Chair: P. Bouyer
Room A

10:30am - 12:30am Finite model theory & Counting logic

Chair: N. Schweikardt
Room A

Higher-order logic & Proof theory

Chair: D. Miller
Room B

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

Homotopy theory

Chair: J. Goubault-Larrecq
Room B

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

Category theory

Chair: P.-A. Melliès
Room B

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

Tuesday 25th June 2019

8am - 9am Coffee and pastries
9am - 10am Invited talk: Peter Selinger
Number-theoretic methods in quantum computing

Chair: S. Abramsky
Room A

10:30am - 12pm Quantum computing

Chair: P. Selinger
Room A

Description and Horn logics

Chair: A. Dawar
Room B

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

4pm - 5pm Category theory

Chair: S.-Y. Katsumata
Room A


Chair: J. Worrell
Room B

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

Wednesday 26th June 2019

8am - 9am Coffee and pastries
9am - 11am Invited tutorial: Daniela Petrisan
A categorical approach to automata theory

Chair: A. Pitts
Room A

11:30am - 12:30pm Category theory

Chair: A. Polonsky
Room A

Modal and temporal logics

Chair: I. Walukiewicz
Room B

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

Constraint satisfaction problems

Chair: A. Bulatov
Room B

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

Dynamic logic and applications

Chair: M. Randour
Room B

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

Thursday 27th June 2019

8am - 9am Coffee and pastries
9am - 10am Invited talk: James Worrell
Orbit Problems for Linear Dynamical Systems

Chair: S. Schmitz
Room A

10:30am - 12:30pm Quantitative verification & Games

Chair: C. Haase
Room A

Quantum computing

Chair: J. Vicary
Room B

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

Probabilistic reasoning & Security

Chair: P. Panangaden
Room B

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

Category theory

Chair: U. Dal Lago
Room B

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