LICS’23 Program:

Mon 26, Tue 27, Wed 28, Thu 29

Monday 26/06

8:15- 9:00 Breakfast

9:00-10:30 Tutorial: Logic for Explainable AI, Adnan Darwiche

10:30- 11:00 Coffee break

11:00-12:30 Finite model theory

• The Descriptive Complexity of Graph Neural Networks, Martin Grohe (Distinguished Paper)
• The Iteration Number of the Weisfeiler-Leman Algorithm, Martin Grohe, Moritz Lichter and Daniel Neuen
• Simulating Logspace-Recursion with Logarithmic Quantifier Depth, Steffen van Bergerem, Martin Grohe, Sandra Kiefer and Luca Oeljeklaus
• Embedded Finite Models beyond Restricted Quantifier Collapse, Michael Benedikt and Ehud Hrushovski
• Distal combinatorial tools for graphs of bounded twin-width, Wojciech Przybyszewski
• A categorical account of composition methods in logic, Dan Marsden, Tomáš Jakl and Nihil Shah

12:30- 14:00 Lunch

14:00-15:30 Logics and verification

• The Logic of Prefixes and Suffixes is Elementary under Homogeneity, Dario Della Monica, Angelo Montanari, Gabriele Puppis and Pietro Sala
• Revisiting Membership Problems in Subclasses of Rational Relations, Pascal Bergsträßer and Moses Ganardi
• PDL on Steroids, Diego Figueira, Santiago Figueira and Edwin Pin Baque
• Verifying linear temporal specifications of constant-rate multi-mode systems, Michael Blondin, Philip Offtermatt and Alex Sansfaçon-Buchanan
• Minimization of Dynamical Systems over Monoids, Georgios Argyris, Alberto Lluch Lafuente, Alexander Leguizamon Robayo, Mirco Tribastone, Max Tschaikowski and Andrea Vandin
• A Higher-Order Indistinguishability Logic for Cryptographic Reasoning, David Baelde, Adrien Koutsos and Joseph Lallemand

15:30- 16:00 Coffee break

16:00- 17:00 Semantic games and bicategories

• Making Concurrency Functional, Glynn Winskel
• From Thin Concurrent Games to Generalized Species of Structures, Pierre Clairambault, Federico Olimpieri and Hugo Paquet
• The Cartesian Closed Bicategory of Thin Spans of Groupoids, Pierre Clairambault and Simon Forest
• Fixpoint operators for 2-categorical structures, Zeinab Galal

17:15- 18:00 Semantics

• A metalanguage for cost-aware denotational semantics, Yue Niu and Robert Harper
• Deterministic stream-sampling for probabilistic programming: semantics and verification, Fredrik Dahlqvist, Alexandra Silva and William Smith
• Automatic Amortized Resource Analysis with Regular Recursive Types, Jessie Grosen, David M. Kahn and Jan Hoffmann

18:30 Reception and distinguished papers announcements

Tuesday 27/06

8:15- 9:00 Breakfast

9:00- 10:30 MSO, transducers, automata

• Folding interpretations, Mikołaj Bojańczyk
• On the growth rates of polyregular functions, Mikołaj Bojańczyk
• Z-polyregular functions, Gaëtan Douéneau-Tabot, Aliaume Lopez and Thomas Colcombet
• Quantifying over Trees in Monadic Second-Order Logic, Massimo Benerecetti, Bozzelli Laura, Fabio Mogavero and Adriano Peron
• Expressive Completeness of Two-Variable First-Order Logic with Counting for First-Order Queries on Unranked Trees, Jelle Hellings, Marc Gyssens, Jan Van den Bussche and Dirk Van Gucht
• Group separation strikes back, Thomas Place and Marc Zeitoun

10:30- 11:00 Coffee break

11:00- 12:30 Proof systems, modal logic

• Intuitionistic S4 is decidable, Marianna Girlando, Roman Kuznets, Sonia Marin, Marianela Morales Elena and Lutz Straßburger
• Cut-restriction: from cuts to analytic cuts, Agata Ciabattoni, Timo Lang and Revantha Ramanayake
• Existential Calculi of Relations with Transitive Closure: Complexity and Edge Saturations, Yoshiki Nakamura
• Simplicial Set Models for Distributed Knowledge, Éric Goubault, Roman Kniazev, Jérémy Ledent and Sergio Rajsbaum
• Fixed Point Logics on Hemimetric Spaces, David Fernández-Duque and Quentin Gougeon
• Computational expressivity of (circular) proofs with fixed points, Gianluca Curzi and Anupam Das

12:30- 14:00 Lunch

14:00- 15:30 Tutorial: Commutativity in Automated Program Verification, Azadeh Farzan

15:30- 16:00 Coffee break

16:00- 17:00 Stochastic systems

• The Probabilistic Rabin Tree Theorem, Damian Niwinski, Paweł Parys and Michał Skrzypczak
• Stopping Criteria for Value Iteration on Stochastic Games with Quantitative Objectives, Jan Kretinsky, Tobias Meggendorfer and Maximilian Weininger
• Stochastic Best-Effort Strategies for Borel Goals, Benjamin Aminof, Giuseppe De Giacomo, Sasha Rubin and Florian Zuleger
• On Certificates, Expected Runtimes, and Termination in Probabilistic Pushdown Automata, Tobias Winkler and Joost-Pieter Katoen

17:15- 18:15 Randomness

• Pseudorandom Finite Models, Jan Dreier and Jamie Tucker-Foltz
• On Exact Sampling in the Two-Variable Fragment of First-Order Logic, Yuanhong Wang, Juhua Pu, Yuyi Wang and Ondrej Kuzelka
• ωPAP Spaces: Reasoning Denotationally About Higher-Order, Recursive Probabilistic and Differentiable Programs, Mathieu Huot, Alexander K. Lew, Vikash K. Mansinghka and Sam Staton (Distinguished Paper)
• Evidential Decision Theory via Partial Markov Categories, Elena Di Lavore and Mario Román

Wednesday 28/06

8:15- 9:00 Breakfast

9:00-10:00 Invited talk: A Survey of Algebraic Proof Complexity: Theory and Applications,Toniann Pitassi

10:00- 10:30 Coffee break

10:30- 12:00 Decidability and complexity

• The Identity Problem in the special affine group of $\mathbb{Z}^2$, Ruiwen Dong (Kleene Award Paper)
• Orbit-finite linear programming, Arka Ghosh, Piotr Hofman and Sławomir Lasota (Distinguished Paper)
• Reachability in Injective Piecewise Affine Maps, Faraz Ghahremani, Edon Kelmendi and Joel Ouaknine
• Multiplicity Problems on Algebraic Series and Context-Free Grammars, Nikhil Balaji, Lorenzo Clemente, Klara Nosan, Mahsa Shirmohammadi and James Worrell
• Structure-Aware Lower Bounds and Broadening the Horizon of Tractability for QBF, Johannes K. Fichte, Robert Ganian, Markus Hecher, Friedrich Slivovsky and Sebastian Ordyniak
• The Power of Positivity, Toghrul Karimov, Edon Kelmendi, Joris Nieuwveld, Joël Ouaknine and James Worrell

12:00- 14:00 Lunch

14:00- 15:00 Invited talk: Applications of Information Inequalities to Database Theory Problems, Dan Suciu

15:00- 15:30 Coffee break

15:30- 16:30 Weighted automata, CSP

• The Big-O Problem for Max-Plus Automata is Decidable (PSPACE-Complete), Laure Daviaud and David Purser
• Computing the linear hull: Deciding Sequential? and Unambiguous? for weighted automata over fields, Jason Bell and Daniel Smertnig
• Boolean symmetric vs. functional PCSP dichotomy, Tamio-Vesa Nakajima and Stanislav Živný
• Symmetries of graphs and structures that fail to interpret a finite thing, Libor Barto, Bertalan Bodor, Marcin Kozik, Antoine Mottet and Michael Pinsker (Distinguished Paper)

16:45- 18:15 Poster session

19:00 Banquet

Thursday 29/06

8:15- 9:00 Breakfast

9:00- 10:00 Invited talk: A system of inference based on proof search: an extended abstract, Dale Miller

10:00- 10:30 Test-of-Time awards

10:30- 11:00 Coffee break

11:00- 12:30 Semantics and rewriting

• Operational Algorithmic Game Semantics, Benedict Bunting and Andrzej Murawski
• Weak Similarity in Higher-Order Mathematical Operational Semantics, Henning Urbat, Stelios Tsampas, Sergey Goncharov, Stefan Milius and Lutz Schröder
• Fully Abstract Normal Form Bisimulation for call-by-value PCF, Nikos Tzevelekos, Vasileios Koutavas and Yu-Yang Lin (Distinguished Paper)
• Central Submonads and Notions of Computation: Soundness, Completeness and Internal Languages, Titouan Carette, Louis Lemonnier and Vladimir Zamdzhiev
• Allegories of Symbolic Manipulation, Francesco Gavazzo
• Higher-dimensional subdiagram matching, Amar Hadzihasanovic and Diana Kessler

12:30- 14:00 Lunch

14:00- 15:00 Linear logic, homotopy theory

• Taylor Expansion as a Monad in Models of DiLL, Marie Kerjean and Jean-Simon Lemay
• Cartesian Coherent Differential Categories, Aymeric Walch and Thomas Ehrhard
• Formalizing $\pi_4(S^3) \cong Z/2Z$ and Computing a Brunerie Number in Cubical Agda, Axel Ljungström and Anders Mörtberg (Distinguished Paper)
• Set-Theoretic and Type-Theoretic Ordinals Coincide, Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg and Chuangjie Xu

15:00- 15:30 Coffee break

15:30- 16:30 Pi-calculus and quantum circuits

• Extensional and Non-extensional Functions as Processes, Ken Sakayori and Davide Sangiorgi (Distinguished Paper)
• A Complete Equational Theory for Quantum Circuits, Alexandre Clément, Nicolas Heurtel, Shane Mansfield, Simon Perdrix and Benoît Valiron
• Completeness for arbitrary finite dimensions of ZXW-calculus, a unifying calculus, Boldizsár Poór, Quanlong Wang, Razin Shaikh, Lia Yeh, Richie Yeung and Bob Coecke
• Complete Graphical Language for Hermiticity-Preserving Superoperators, Renaud Vilmart, Titouan Carette, Timothée Hoffreumon and Émile Larroque