Anuj Dawar and Erich Grädel | Preface | | |

Michael Blondin, Javier Esparza, Stefan Jaax and Antonin Kučera | Black Ninjas in the Dark: Formal Analysis of Population Protocols | | |

Thierry Coquand | Inner Models of Univalence | | |

Peter O'Hearn | Continuous Reasoning: Scaling the Impact of Formal Methods | | |

Ki Yung Ahn, Ross Horne, Shang-Wei Lin and Alwen Tiu | Quasi-Open Bisimilarity with Mismatch is Intuitionistic | | Jul 09 15:00 |

S. Akshay, Blaise Genest and Nikhil Vyas | Distribution-based objectives for Markov Decision Processes | | Jul 10 15:40 |

Joel Allred and Ulrich Ultes-Nitsche | A Simple and Optimal Complementation Algorithm for Büchi Automata | | Jul 09 16:20 |

Robert Atkey | The Syntax and Semantics of Quantitative Type Theory | | Jul 11 12:20 |

Albert Atserias and Joanna Ochremiak | Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism Problem | | Jul 12 12:20 |

Steve Awodey, Jonas Frey and Sam Speight | Impredicative Encodings of (Higher) Inductive Types | | Jul 10 11:00 |

Christel Baier, Nathalie Bertrand, Clemens Dubslaff, Daniel Gburek and Ocan Sankur | Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes | | Jul 10 16:00 |

Valentin Blot and James Laird | Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types | | Jul 11 11:20 |

Manuel Bodirsky, Florent Madelaine and Antoine Mottet | A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP | | Jul 11 11:20 |

Brandon Bohrer and André Platzer | A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow | | Jul 12 15:00 |

Mikolaj Bojanczyk, Laure Daviaud and Krishna Shankara Narayanan | Regular and First Order List Functions | | Jul 09 12:20 |

Mikołaj Bojańczyk, Martin Grohe and Michał Pilipczuk | Definable decompositions for graphs of bounded linear cliquewidth | | Jul 09 11:00 |

Mikołaj Bojańczyk and Szymon Toruńczyk | On computability and tractability for infinite sets | | Jul 12 12:00 |

Udi Boker and Yariv Shaulian | Automaton-Based Criteria for Membership in CTL | | Jul 09 17:00 |

Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski and Fabio Zanasi | Rewriting with Frobenius | | Jul 12 15:00 |

Filippo Bonchi, Pierre Ganty, Roberto Giacobazzi and Dusko Pavlovic | Sound up-to techniques and Complete abstract domains | | Jul 09 17:00 |

Tomas Brazdil, Krishnendu Chatterjee, Antonin Kucera, Petr Novotný, Dominik Velan and Florian Zuleger | Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS | | Jul 12 14:40 |

Roberto Bruni, Hernan Melgratti and Ugo Montanari | Concurrency and Probability: Removing Confusion, Compositionally | | Jul 09 14:00 |

Ulrik Buchholtz, Floris van Doorn and Egbert Rijke | Higher Groups in Homotopy Type Theory | | Jul 09 12:00 |

Simon Castellan, Pierre Clairambault, Hugo Paquet and Glynn Winskel | The concurrent game semantics of Probabilistic PCF | | Jul 10 16:20 |

Yijia Chen and Jörg Flum | Tree depth, quantifier elimination, and quantifier rank | | Jul 10 11:40 |

Yijia Chen, Moritz Mueller and Keita Yokoyama | A parameterized halting problem, the linear time hierarchy, and the MRDP theorem | | Jul 09 12:00 |

Liron Cohen, Vincent Rahli, Mark Bickford and Robert Constable | Computability Beyond Church-Turing via Choice Sequences | | Jul 11 12:00 |

Thierry Coquand, Simon Huber and Anders Mörtberg | On Higher Inductive Types in Cubical Type Theory | | Jul 11 10:20 |

Karl Crary | Strong Sums in Focused Logic | | Jul 09 12:20 |

Raphaëlle Crubillé | Probabilistic stable functions on discrete cones are power series. | | Jul 12 14:00 |

Daniel Danielski and Emanuel Kieronski | Unary negation fragment with equivalence relations has the finite model property | | Jul 11 11:40 |

Luc Dartois, Emmanuel Filiot and Nathan Lhote | Logics for Word Transductions with Synthesis | | Jul 10 14:40 |

Ankush Das, Jan Hoffmann and Frank Pfenning | Work Analysis with Resource-Aware Session Types | | Jul 10 11:40 |

Vrunda Dave, Paul Gastin and Krishna S | Regular Transducer Expressions for Regular Transformations over infinite words | | Jul 09 17:40 |

Laure Daviaud, Marcin Jurdzinski and Ranko Lazic | A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games | | Jul 09 14:20 |

Nadish de Silva | Logical paradoxes in quantum computation | | Jul 12 09:20 |

Romain Demangeon and Nobuko Yoshida | Causal Computational Complexity of Distributed Processes | | Jul 09 15:20 |

Arnaud Durand, Anselm Haak and Heribert Vollmer | Model-Theoretic Characterizations of Boolean and Arithmetic Circuit Classes of Small Depth | | Jul 10 11:20 |

Adrien Durier, Daniel Hirschkoff and Davide Sangiorgi | Eager Functions as Processes | | Jul 09 14:40 |

Clovis Eberhart and Tom Hirschowitz | What's in a game? A theory of game models | | Jul 10 15:40 |

Javier Esparza, Jan Kretinsky and Salomon Sickert | One Theorem to Rule Them All: A Unified Translation of LTL into $\omega$-Automata | | Jul 09 16:00 |

Thomas Ferrère, Thomas A Henzinger and N Ege Sarac | A Theory of Register Monitors | | Jul 12 14:20 |

Diego Figueira and M. Praveen | Playing with Repetitions in Data Words Using Energy Games | | Jul 09 15:00 |

Nathanaël Fijalkow | The State Complexity of Alternating Automata | | Jul 09 16:40 |

Emmanuel Filiot, Raffaella Gentilini and Jean-Francois Raskin | Rational Synthesis Under Imperfect Information | | Jul 09 14:40 |

Dror Fried, Axel Legay, Joel Ouaknine and Moshe Y Vardi | Sequential Relational Decomposition | | Jul 09 11:40 |

Dan Frumin, Robbert Krebbers and Lars Birkedal | ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency | | Jul 09 14:20 |

Francesco Gavazzo | Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances | | Jul 12 09:00 |

Guillaume Geoffroy | Classical realizability as a classifier for nondeterminism | | Jul 10 12:20 |

Neil Ghani, Jules Hedges, Viktor Winschel and Philipp Zahn | Compositional game theory | | Jul 09 15:20 |

Adrien Guatto | A Generalized Modality for Recursion | | Jul 12 09:20 |

Grzegorz Głuch, Jerzy Marcinkowski and Piotr Ostropolski-Nalewaja | Can One Escape Red Chains? Regular Path Queries Determinacy is Undecidable. | | Jul 11 12:20 |

Amar Hadzihasanovic, Kang Feng Ng and Quanlong Wang | Two complete axiomatisations of pure-state qubit quantum computing | | Jul 12 10:00 |

Michael Hahn, Andreas Krebs and Howard Straubing | Wreath Products of Distributive Forest Algebras | | Jul 10 12:00 |

Kuen-Bang Hou and Ulrik Buchholtz | Cellular Cohomology in Homotopy Type Theory | | Jul 09 11:20 |

Ehud Hrushovski, Joel Ouaknine, Amaury Pouly and James Worrell | Polynomial Invariants for Affine Programs | | Jul 10 10:00 |

Dominic Hughes | Unification nets: canonical proof net quantifiers | | Jul 10 14:40 |

Pawel Idziak and Jacek Krzaczkowski | Satisfiability in multi-valued circuits | | Jul 11 12:00 |

Emmanuel Jeandel, Simon Perdrix and Renaud Vilmart | A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics | | Jul 12 09:40 |

Emmanuel Jeandel, Simon Perdrix and Renaud Vilmart | Diagrammatic Reasoning beyond Clifford+T Quantum Mechanics | | Jul 12 10:20 |

Bruce Kapron and Florian Steinberg | Type-two polynomial-time and restricted lookahead. | | Jul 10 15:00 |

Marie Kerjean | A Logical Account for Linear Partial Differential Equations | | Jul 10 14:20 |

Nicolai Kraus and Thorsten Altenkirch | Free Higher Groups in Homotopy Type Theory | | Jul 09 11:40 |

Jan Kretinsky and Tobias Meggendorfer | Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes | | Jul 10 16:20 |

Antti Kuusisto and Carsten Lutz | Weighted model counting beyond two-variable logic | | Jul 11 11:00 |

Olivier Laurent | Around Classical and Intuitionistic Linear Logics | | Jul 10 15:00 |

Karoliina Lehtinen | A modal mu perspective on solving parity games in quasipolynomial time. | | Jul 09 14:00 |

Thomas Leventis | Probabilistic Böhm Trees and Probabilistic Separation | | Jul 09 17:40 |

Bert Lindenhovius, Michael Mislove and Vladimir Zamdzhiev | Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams | | Jul 09 16:00 |

Radu Mardare, Prakash Panangaden, Dexter Kozen, Dana Scott, Robert Furber and Giorgio Bacci | Boolean-Valued Semantics for Stochastic Lambda-Calculus | | Jul 09 16:40 |

Radu Mardare, Prakash Panangaden, Gordon Plotkin and Giorgio Bacci | An algebraic theory of Markov processes | | Jul 09 16:20 |

Paul-André Melliès | Ribbon tensorial logic | | Jul 12 15:20 |

Paul-André Melliès and Léo Stefanesco | An Asynchronous Soundness Theorem for Concurrent Separation Logic | | Jul 10 16:00 |

Matteo Mio | Riesz Modal Logic with Threshold Operators | | Jul 10 14:20 |

Étienne Miquey | A sequent calculus with dependent types for classical arithmetic | | Jul 11 10:00 |

Benoit Monin | An answer to the Gamma question | | Jul 10 10:20 |

Sean Moss and Tamara von Glehn | Dialectica models of type theory | | Jul 11 11:00 |

Koko Muroya, Wai-Tak Cheung and Dan Ghica | The Geometry of Computation-Graph Abstraction | | Jul 12 10:00 |

Yoji Nanjo, Hiroshi Unno, Eric Koskinen and Tachio Terauchi | Dependent Temporal Effects and Fixpoint Logic for Verification | | Jul 11 11:40 |

Matthias Niewerth | MSO Queries on Trees: Enumerating Answers under Updates Using Forest Algebras | | Jul 10 12:20 |

Andreas Nuyts and Dominique Devriese | Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory | | Jul 12 10:20 |

Michał Pilipczuk, Sebastian Siebertz and Szymon Toruńczyk | Parameterized circuit complexity of model-checking on sparse structures | | Jul 09 11:20 |

Michał Pilipczuk, Sebastian Siebertz and Szymon Toruńczyk | On the number of types in sparse graphs | | Jul 10 11:00 |

Maciej Piróg, Tom Schrijvers, Nicolas Wu and Mauro Jaskelioff | Syntax and Semantics for Operations with Scopes | | Jul 12 14:40 |

André Platzer and Yong Kiam Tan | Differential Equation Axiomatization: The Impressive Power of Differential Ghosts | | Jul 12 15:20 |

Damien Pous and Valeria Vignudelli | Allegories: decidability and graph homomorphisms | | Jul 12 14:20 |

Thomas Powell | A functional interpretation with state | | Jul 12 09:40 |

Colin Riba and Pierre Pradic | LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic | | Jul 10 14:00 |

Benjamin Sherman, Luke Sciarappa, Michael Carbin and Adam Chlipala | Computable decision-making on the reals and other spaces via partiality and nondeterminism | | Jul 12 14:00 |

Kristina Sojakova and Patricia Johann | A General Framework for Relational Parametricity | | Jul 10 12:00 |

Jonathan Sterling and Robert Harper | Guarded Computational Type Theory | | Jul 10 11:20 |

Takeshi Tsukada, Kazuyuki Asada and Luke Ong | Species, Profunctors and Taylor Expansion Weighted by SMCC--A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs-- | | Jul 12 09:00 |

Pierre Vial | Every λ-Term is Meaningful for the Infinitary Relational Model | | Jul 09 17:20 |

Paul Wild, Lutz Schröder, Dirk Pattinson and Barbara König | A van Benthem Theorem for Fuzzy Modal Logic | | Jul 10 14:00 |

Noam Zeilberger | A theory of linear typings as flows on 3-valent graphs | | Jul 09 11:00 |

Georg Zetzsche | PTL-separability and closures for WQOs on words | | Jul 09 17:20 |