| Authors | Title | Paper | Talk |
|---|
| 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 |