LICS 2025 Programme

Venue: School of Computing (Building COM1, Medium Level 2), National University of Singapore, 13 Computing Drive, Singapore 117417 (link to local info)

Monday, 23 June 2025

Seminar Room 1

08:30-09:00 Registration (Foyer)
09:00-10:00 Invited Talk: Anuj Dawar. Notions of Width: Variables, Pebbles and Supports
10:00-10:40 Tea Break
10:40-11:00 Andrei Popescu. Completing Gordon's Higher-Order Logic
11:00-11:20 Liron Cohen, Ariel Grunfeld, Dominik Kirst, Étienne Miquey. Syntactic Effectful Realizability in Higher-Order Logic
11:20-11:40 Max Bannach, Erik D. Demaine, Timothy Gomez and Markus Hecher. #P is Sandwiched by One and Two #2DNF Calls: Is Subtraction Stronger Than We Thought?
11:40-12:00 Mikhail Starchak. Quantifier Elimination for Regular Integer Linear-Exponential Programming
12:00-13:30 Lunch
13:30-13:50 Florian Frank, Daniel Hausmann, Stefan Milius, Lutz Schröder and Henning Urbat. Alternating Nominal Automata with Name Allocation
13:50-14:10 Mayuko Kori, Kazuki Watanabe and Jurriaan Rot. Initial Algebra Correspondence under Reachability Conditions
14:10-14:30 Thomas Ehrhard, Farzad Jafarrahmani and Alexis Saurin. On the denotation of circular and non-wellfounded proofs in linear logic with fixed points
14:30-14:50 Mishel Carelli, Bernd Finkbeiner and Julian Siber. Closure and Complexity of Temporal Causality
14:50-15:30 Tea Break
15:30-15:50 Niels van der Weide. The internal languages of univalent categories
15:50-16:10 Daniel Gratzer, Jonathan Weinberger and Ulrik Buchholtz. The Yoneda embedding in simplicial type theory (distinguished paper)
16:10-16:30 Andrew Slattery and Jonathan Sterling. Hofmann-Streicher Lifting of Fibred Categories (distinguished paper)
16:40-17:40 Business Meeting (Seminar Room 2)
18:00 Reception at School of Computing

Seminar Room 3

Logic Mentoring Workshop

Tuesday, 24 June 2025

Seminar Room 1

09:00-10:00 Invited Tutorial: Rustan Leino. Tools for software verification: an industrial perspective
10:00-10:40 Tea Break
10:40-11:00 Johannes Kloibhofer and Yde Venema. Interpolation for the two-way modal μ-calculus
11:00-11:20 Jim de Groot, Ian Shillito and Ranald Clouston. Semantical Analysis of Intuitionistic Modal Logics between CK and IK
11:20-11:40 Victoria Barrett, Alessio Guglielmi, Benjamin Ralph and Lutz Straßburger. Proof Compression via Subatomic Logic and Guarded Substitutions
11:40-12:00 Sanjiv Ranchod and Marcelo Fiore. Substructural Abstract Syntax with Variable Binding and Single-Variable Substitution
12:00-13:30 Lunch
13:30-13:50 Aleksei Tiurin, Chris Barrett, Dan Ghica and Nick Hu. Equivalence Hypergraphs: DPO Rewriting for Monoidal E-Graphs
13:50-14:10 Mirai Ikebuchi. Homological Invariants of Higher-Order Equational Theories
14:10-14:30 Anatole Dahan. Group Order Logic
14:30-14:50 Ruiwen Dong and Corentin Bodart. The Identity Problem in virtually solvable matrix groups over algebraic numbers (distinguished paper)
14:50-15:30 Tea Break
15:30-15:50 Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg and Chuangjie Xu. Ordinal Exponentiation in Homotopy Type Theory (distinguished paper)
15:50-16:10 Thibaut Benjamin, Ioannis Markakis, Wilfred Offord, Chiara Sarti and Jamie Vicary. Naturality for higher-dimensional path types
16:10-16:30 Axel Ljungström and David Wärn. The Steenrod squares via unordered joins (distinguished paper)
16:40-17:40 Awards Session
Test-of-Time-Award Talks:
Joël Ouaknine and James B. Worrell. On the Decidability of Metric Temporal Logic
Benjamin Rossman. Existential Positive Types and Preservation under Homomorphisms

Seminar Room 3

10:40-11:00 Qiaolan Meng, Juhua Pu, Hongting Niu, Yuyi Wang, Yuanhong Wang and Ondřej Kuželka. Model Enumeration of Two-Variable Logic with Quadratic Delay Complexity
11:00-11:20 Thomas Place and Marc Zeitoun. Navigational hierarchies of regular languages
11:20-11:40 Louwe B. Kuijer, Tony Tan, Frank Wolter and Michael Zakharyaschev. Separation and Definability in Fragments of Two-Variable First-Order Logic with Counting
11:40-12:00 Sam M. Thompson, Nicole Schweikardt and Dominik D. Freydenberger. Characterization and Decidability of FC-Definable Regular Languages (distinguished paper)
12:00-13:30 Lunch
13:30-13:50 Antoine Mottet. Algebraic and algorithmic synergies between promise and infinite-domain CSPs
13:50-14:10 Demian Banakh, Lorenzo Ciardo, Marcin Kozik and Jan Tulowiecki. Classical simulation of quantum CSP strategies
14:10-14:30 Paolo Marimon and Michael Pinsker. Binary symmetries of tractable non-rigid structures
14:30-14:50 Johanna Brunar, Marcin Kozik, Tomáš Nagy and Michael Pinsker. The sorrows of a smooth digraph: the first hardness criterion for infinite directed graph-colouring problems
14:50-15:30 Tea Break
15:30-15:50 Quentin Aristote, Sam van Gool, Daniela Petrişan and Mahsa Shirmohammadi. Learning Weighted Automata over Number Rings, Concretely and Categorically
15:50-16:10 Christof Löding and Igor Walukiewicz. Minimal History-Deterministic Co-Büchi Automata: Congruences and Passive Learning (distinguished paper)
16:10-16:30 Prince Mathew, Vincent Penelle and A V Sreejith. Learning Deterministic One-Counter Automata in Polynomial Time

Wednesday, 25 June 2025

Seminar Room 1

09:00-10:00 Invited Talk: Hongseok Yang. Introduction to Razborov's Flag Algebras: Logic-Based Computational Methods in Extremal Combinatorics
10:00-10:40 Tea Break
10:40-11:00 Thomas Brihaye, Krishnendu Chatterjee, Stefanie Mohr and Maximilian Weininger. Risk-aware Markov Decision Processes Using Cumulative Prospect Theory
11:00-11:20 Dario Stein. Random Variables, Conditional Independence and Categories of Abstract Sample Spaces
11:20-11:40 Nathan Bowler, Sergey Goncharov and Paul Blain Levy. Probabilistic Strategies: Definability and the Tensor Completeness Problem
11:40-12:00 Christel Baier, Krishnendu Chatterjee, Tobias Meggendorfer and Jakob Piribauer. Multiplicative Rewards in Markovian Models
12:00-13:30 Lunch
13:30-13:50 Pierre Clairambault. The Qualitative Collapse of Concurrent Games
13:50-14:10 Benedict Bunting and Andrzej Murawski. Reachability Types, Traces and Full Abstraction
14:10-14:30 Filippo Bonchi, Elena Di Lavore and Mario Román. Effectful Mealy Machines: Bisimulation and Trace (distinguished paper)
14:30-14:50 Jonas Forster, Lutz Schröder and Paul Wild. Conformance Games for Graded Semantics
14:50-15:30 Tea Break
15:30-15:50 Marta Grobelna, Jan Křetínský and Maximilian Weininger. Stopping Criteria for Value Iteration on Concurrent Stochastic Reachability and Safety Games
15:50-16:10 Roland Guttenberg, Wojciech Czerwiński and Sławomir Lasota. Reachability and Related Problems in Vector Addition Systems with Nested Zero Tests
16:10-16:30 Yousef Shakiba, Henry Sinclair-Banks and Georg Zetzsche. A Complexity Dichotomy for Semilinear Target Sets in Automata with One Counter
16:40-17:40 Poster Session (Foyer)
18:30 Banquet Dinner (NUSS Guild Hall)
Banquet venue: National University of Singapore Society; Kent Ridge Guild House; Level 2: Cluny, Dalvey & Evans Room; 9 Kent Ridge Drive; Singapore 119241

Seminar Room 3

10:40-11:00 Timothy Bourke, Paul Jeanmaire and Marc Pouzet. Functional Stream Semantics for a Synchronous Block-Diagram Compiler
11:00-11:20 A. R. Balasubramanian, Dmitry Chistikov and Rupak Majumdar. Pushdown Model Checking above the Cubic Bottleneck (distinguished paper)
11:20-11:40 Jasmine Xuereb, Adrian Francalanza and Antonis Achilleos. If At First You Don't Succeed: Extended Monitorability through Multiple Executions
11:40-12:00 Toghrul Karimov, Edon Kelmendi, Joel Ouaknine and James Worrell. Multiple Reachability in Linear Dynamical Systems
12:00-13:30 Lunch
13:30-13:50 Jan Dreier, Robert Ganian and Thekla Hamm. Approximate Evaluation of Quantitative Second Order Queries
13:50-14:10 Mamadou Moustapha Kanté, Bruno Guillon, Eun Jung Kim, Sang-il Oum and Rutger Campbell. Recognisability Equals Definability for Finitely Representable Matroids of Bounded Path-Width
14:10-14:30 Marius Bozga, Radu Iosif and Florian Zuleger. Regular Grammars for Sets of Graphs of Tree-Width 2
14:30-14:50 Mikołaj Bojańczyk and Pierre Ohlmann. Graphs of unbounded linear cliquewidth must transduce all trees
14:50-15:30 Tea Break
15:30-15:50 Leoni Pugh and Jonathan Sterling. When is the partial map classifier a Sierpiński cone?
15:50-16:10 Pedro H. Azevedo de Amorim, Satoshi Kura and Philip Saville. Logical relations for call-by-push-value models, via internal fibrations in a 2-category
16:10-16:30 Aymeric Walch. Compositional Taylor expansion in cartesian differential categories
16:40-17:40 Poster Session (Foyer)
18:30 Banquet Dinner (NUSS Guild Hall)
Banquet venue: National University of Singapore Society; Kent Ridge Guild House; Level 2: Cluny, Dalvey & Evans Room; 9 Kent Ridge Drive; Singapore 119241

Thursday, 26 June 2025

Seminar Room 1

09:00-10:00 Invited Tutorial: Christine Tasson. Linear Logic and probabilistic programming
10:00-10:40 Tea Break
10:40-11:00 Anton Chernev, Corina Cirstea, Helle Hvid Hansen and Clemens Kupke. Thin Coalgebraic Behaviours Are Inductive
11:00-11:20 Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder and Paul Wild. Relators and Notions of Simulation Revisited
11:20-11:40 Paul Wild and Lutz Schröder. Behavioural Conformances based on Lax Couplings
11:40-12:00 Lorenzo Clemente. The commutativity problem for effective varieties of formal series, and applications (distinguished paper)
12:00-13:30 Lunch
13:30-13:50 Sam Adam-Day, Michael Benedikt and Alberto Larrauri. Convergence laws for extensions of first order logic with averaging
13:50-14:10 Jakub Gajarský, Michał Pilipczuk and Filip Pokrývka. 3D-grids are not transducible from planar graphs
14:10-14:30 Petr Hlineny and Jan Jedelský. Transductions of Graph Classes Admitting Product Structure
14:30-14:50 Wojciech Przybyszewski and Szymon Toruńczyk. Flipping and Forking
14:50-15:10 Bert Lindenhovius and Vladimir Zamdzhiev. Operator Spaces, Linear Logic and the Heisenberg-Schrödinger Duality of Quantum Theory
15:10-15:30 Gilles Barthe, Minbo Gao, Theo Wang and Li Zhou. Complete Quantum Relational Hoare Logics from Optimal Transport Duality
15:30-15:50 Dominik Kirst and Haoyi Zeng. The Blurred Drinker Paradox: Constructive Reverse Mathematics of the Downward Löwenheim-Skolem Theorem (distinguished paper)
15:50-16:50 Tea Break
17:30 Bus Transfer from School of Computing to Night Safari

Contact

Barbara König and Lars Birkedal (lics25@easychair.org)