Editors: Anuj Dawar and Erich Grädel

Anuj Dawar and Erich GrädelPreface
Michael Blondin, Javier Esparza, Stefan Jaax and Antonin KučeraBlack Ninjas in the Dark: Formal Analysis of Population Protocols
Thierry CoquandInner Models of Univalence
Peter O'HearnContinuous Reasoning: Scaling the Impact of Formal Methods
Ki Yung Ahn, Ross Horne, Shang-Wei Lin and Alwen TiuQuasi-Open Bisimilarity with Mismatch is IntuitionisticJul 09 15:00
S. Akshay, Blaise Genest and Nikhil VyasDistribution-based objectives for Markov Decision ProcessesJul 10 15:40
Joel Allred and Ulrich Ultes-NitscheA Simple and Optimal Complementation Algorithm for Büchi AutomataJul 09 16:20
Robert AtkeyThe Syntax and Semantics of Quantitative Type TheoryJul 11 12:20
Albert Atserias and Joanna OchremiakDefinable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism ProblemJul 12 12:20
Steve Awodey, Jonas Frey and Sam SpeightImpredicative Encodings of (Higher) Inductive TypesJul 10 11:00
Christel Baier, Nathalie Bertrand, Clemens Dubslaff, Daniel Gburek and Ocan SankurStochastic Shortest Paths and Weight-Bounded Properties in Markov Decision ProcessesJul 10 16:00
Valentin Blot and James LairdExtensional and Intensional Semantic Universes: A Denotational Model of Dependent TypesJul 11 11:20
Manuel Bodirsky, Florent Madelaine and Antoine MottetA universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNPJul 11 11:20
Brandon Bohrer and André PlatzerA Hybrid, Dynamic Logic for Hybrid-Dynamic Information FlowJul 12 15:00
Mikolaj Bojanczyk, Laure Daviaud and Krishna Shankara NarayananRegular and First Order List FunctionsJul 09 12:20
Mikołaj Bojańczyk, Martin Grohe and Michał PilipczukDefinable decompositions for graphs of bounded linear cliquewidthJul 09 11:00
Mikołaj Bojańczyk and Szymon ToruńczykOn computability and tractability for infinite setsJul 12 12:00
Udi Boker and Yariv ShaulianAutomaton-Based Criteria for Membership in CTLJul 09 17:00
Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski and Fabio ZanasiRewriting with FrobeniusJul 12 15:00
Filippo Bonchi, Pierre Ganty, Roberto Giacobazzi and Dusko PavlovicSound up-to techniques and Complete abstract domainsJul 09 17:00
Tomas Brazdil, Krishnendu Chatterjee, Antonin Kucera, Petr Novotný, Dominik Velan and Florian ZulegerEfficient Algorithms for Asymptotic Bounds on Termination Time in VASSJul 12 14:40
Roberto Bruni, Hernan Melgratti and Ugo MontanariConcurrency and Probability: Removing Confusion, CompositionallyJul 09 14:00
Ulrik Buchholtz, Floris van Doorn and Egbert RijkeHigher Groups in Homotopy Type TheoryJul 09 12:00
Simon Castellan, Pierre Clairambault, Hugo Paquet and Glynn WinskelThe concurrent game semantics of Probabilistic PCFJul 10 16:20
Yijia Chen and Jörg FlumTree depth, quantifier elimination, and quantifier rankJul 10 11:40
Yijia Chen, Moritz Mueller and Keita YokoyamaA parameterized halting problem, the linear time hierarchy, and the MRDP theoremJul 09 12:00
Liron Cohen, Vincent Rahli, Mark Bickford and Robert ConstableComputability Beyond Church-Turing via Choice SequencesJul 11 12:00
Thierry Coquand, Simon Huber and Anders MörtbergOn Higher Inductive Types in Cubical Type TheoryJul 11 10:20
Karl CraryStrong Sums in Focused LogicJul 09 12:20
Raphaëlle CrubilléProbabilistic stable functions on discrete cones are power series.Jul 12 14:00
Daniel Danielski and Emanuel KieronskiUnary negation fragment with equivalence relations has the finite model propertyJul 11 11:40
Luc Dartois, Emmanuel Filiot and Nathan LhoteLogics for Word Transductions with SynthesisJul 10 14:40
Ankush Das, Jan Hoffmann and Frank PfenningWork Analysis with Resource-Aware Session TypesJul 10 11:40
Vrunda Dave, Paul Gastin and Krishna SRegular Transducer Expressions for Regular Transformations over infinite wordsJul 09 17:40
Laure Daviaud, Marcin Jurdzinski and Ranko LazicA pseudo-quasi-polynomial algorithm for solving mean-payoff parity gamesJul 09 14:20
Nadish de SilvaLogical paradoxes in quantum computationJul 12 09:20
Romain Demangeon and Nobuko YoshidaCausal Computational Complexity of Distributed ProcessesJul 09 15:20
Arnaud Durand, Anselm Haak and Heribert VollmerModel-Theoretic Characterizations of Boolean and Arithmetic Circuit Classes of Small DepthJul 10 11:20
Adrien Durier, Daniel Hirschkoff and Davide SangiorgiEager Functions as ProcessesJul 09 14:40
Clovis Eberhart and Tom HirschowitzWhat's in a game? A theory of game modelsJul 10 15:40
Javier Esparza, Jan Kretinsky and Salomon SickertOne Theorem to Rule Them All: A Unified Translation of LTL into $\omega$-AutomataJul 09 16:00
Thomas Ferrère, Thomas A Henzinger and N Ege SaracA Theory of Register MonitorsJul 12 14:20
Diego Figueira and M. PraveenPlaying with Repetitions in Data Words Using Energy GamesJul 09 15:00
Nathanaël FijalkowThe State Complexity of Alternating AutomataJul 09 16:40
Emmanuel Filiot, Raffaella Gentilini and Jean-Francois RaskinRational Synthesis Under Imperfect InformationJul 09 14:40
Dror Fried, Axel Legay, Joel Ouaknine and Moshe Y VardiSequential Relational DecompositionJul 09 11:40
Dan Frumin, Robbert Krebbers and Lars BirkedalReLoC: A Mechanised Relational Logic for Fine-Grained ConcurrencyJul 09 14:20
Francesco GavazzoQuantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative DistancesJul 12 09:00
Guillaume GeoffroyClassical realizability as a classifier for nondeterminismJul 10 12:20
Neil Ghani, Jules Hedges, Viktor Winschel and Philipp ZahnCompositional game theoryJul 09 15:20
Adrien GuattoA Generalized Modality for RecursionJul 12 09:20
Grzegorz Głuch, Jerzy Marcinkowski and Piotr Ostropolski-NalewajaCan One Escape Red Chains? Regular Path Queries Determinacy is Undecidable.Jul 11 12:20
Amar Hadzihasanovic, Kang Feng Ng and Quanlong WangTwo complete axiomatisations of pure-state qubit quantum computingJul 12 10:00
Michael Hahn, Andreas Krebs and Howard StraubingWreath Products of Distributive Forest AlgebrasJul 10 12:00
Kuen-Bang Hou and Ulrik BuchholtzCellular Cohomology in Homotopy Type TheoryJul 09 11:20
Ehud Hrushovski, Joel Ouaknine, Amaury Pouly and James WorrellPolynomial Invariants for Affine ProgramsJul 10 10:00
Dominic HughesUnification nets: canonical proof net quantifiersJul 10 14:40
Pawel Idziak and Jacek KrzaczkowskiSatisfiability in multi-valued circuitsJul 11 12:00
Emmanuel Jeandel, Simon Perdrix and Renaud VilmartA Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum MechanicsJul 12 09:40
Emmanuel Jeandel, Simon Perdrix and Renaud VilmartDiagrammatic Reasoning beyond Clifford+T Quantum MechanicsJul 12 10:20
Bruce Kapron and Florian SteinbergType-two polynomial-time and restricted lookahead.Jul 10 15:00
Marie KerjeanA Logical Account for Linear Partial Differential EquationsJul 10 14:20
Nicolai Kraus and Thorsten AltenkirchFree Higher Groups in Homotopy Type TheoryJul 09 11:40
Jan Kretinsky and Tobias MeggendorferConditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision ProcessesJul 10 16:20
Antti Kuusisto and Carsten LutzWeighted model counting beyond two-variable logicJul 11 11:00
Olivier LaurentAround Classical and Intuitionistic Linear LogicsJul 10 15:00
Karoliina LehtinenA modal mu perspective on solving parity games in quasipolynomial time.Jul 09 14:00
Thomas LeventisProbabilistic Böhm Trees and Probabilistic SeparationJul 09 17:40
Bert Lindenhovius, Michael Mislove and Vladimir ZamdzhievEnriching a Linear/Non-linear Lambda Calculus: A Programming Language for String DiagramsJul 09 16:00
Radu Mardare, Prakash Panangaden, Dexter Kozen, Dana Scott, Robert Furber and Giorgio BacciBoolean-Valued Semantics for Stochastic Lambda-CalculusJul 09 16:40
Radu Mardare, Prakash Panangaden, Gordon Plotkin and Giorgio BacciAn algebraic theory of Markov processesJul 09 16:20
Paul-André MellièsRibbon tensorial logicJul 12 15:20
Paul-André Melliès and Léo StefanescoAn Asynchronous Soundness Theorem for Concurrent Separation LogicJul 10 16:00
Matteo MioRiesz Modal Logic with Threshold OperatorsJul 10 14:20
Étienne MiqueyA sequent calculus with dependent types for classical arithmeticJul 11 10:00
Benoit MoninAn answer to the Gamma questionJul 10 10:20
Sean Moss and Tamara von GlehnDialectica models of type theoryJul 11 11:00
Koko Muroya, Wai-Tak Cheung and Dan GhicaThe Geometry of Computation-Graph AbstractionJul 12 10:00
Yoji Nanjo, Hiroshi Unno, Eric Koskinen and Tachio TerauchiDependent Temporal Effects and Fixpoint Logic for VerificationJul 11 11:40
Matthias NiewerthMSO Queries on Trees: Enumerating Answers under Updates Using Forest AlgebrasJul 10 12:20
Andreas Nuyts and Dominique DevrieseDegrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type TheoryJul 12 10:20
Michał Pilipczuk, Sebastian Siebertz and Szymon ToruńczykParameterized circuit complexity of model-checking on sparse structuresJul 09 11:20
Michał Pilipczuk, Sebastian Siebertz and Szymon ToruńczykOn the number of types in sparse graphsJul 10 11:00
Maciej Piróg, Tom Schrijvers, Nicolas Wu and Mauro JaskelioffSyntax and Semantics for Operations with ScopesJul 12 14:40
André Platzer and Yong Kiam TanDifferential Equation Axiomatization: The Impressive Power of Differential GhostsJul 12 15:20
Damien Pous and Valeria VignudelliAllegories: decidability and graph homomorphismsJul 12 14:20
Thomas PowellA functional interpretation with stateJul 12 09:40
Colin Riba and Pierre PradicLMSO: A Curry-Howard Approach to Church's Synthesis via Linear LogicJul 10 14:00
Benjamin Sherman, Luke Sciarappa, Michael Carbin and Adam ChlipalaComputable decision-making on the reals and other spaces via partiality and nondeterminismJul 12 14:00
Kristina Sojakova and Patricia JohannA General Framework for Relational ParametricityJul 10 12:00
Jonathan Sterling and Robert HarperGuarded Computational Type TheoryJul 10 11:20
Takeshi Tsukada, Kazuyuki Asada and Luke OngSpecies, Profunctors and Taylor Expansion Weighted by SMCC--A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs--Jul 12 09:00
Pierre VialEvery λ-Term is Meaningful for the Infinitary Relational ModelJul 09 17:20
Paul Wild, Lutz Schröder, Dirk Pattinson and Barbara KönigA van Benthem Theorem for Fuzzy Modal LogicJul 10 14:00
Noam ZeilbergerA theory of linear typings as flows on 3-valent graphsJul 09 11:00
Georg ZetzschePTL-separability and closures for WQOs on wordsJul 09 17:20