Title/Authors  Title  Research Artifacts
[?] A research
artifact is any byproduct of a research project that is not
directly included in the published research paper. In Computer
Science research this is often source code and data sets, but
it could also be media, documentation, inputs to proof
assistants, shellscripts to run experiments, etc.

Details 

One Theorem to Rule Them All: A Unified Translation of LTL into ωAutomata Javier Esparza, Jan Kretínský, Salomon Sickert 
One Theorem to Rule Them All: A Unified Translation of LTL into ωAutomata Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Conditional ValueatRisk for Reachability and Mean Payoff in Markov Decision Processes Jan Kretínský, Tobias Meggendorfer 
Conditional ValueatRisk for Reachability and Mean Payoff in Markov Decision Processes Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

An Algebraic Theory of Markov Processes Giorgio Bacci, Radu Mardare, Prakash Panangaden, Gordon D. Plotkin 
An Algebraic Theory of Markov Processes Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

The State Complexity of Alternating Automata Nathanaël Fijalkow 
The State Complexity of Alternating Automata Details 

Discussion Comments:
0
Verification:
Author has
not verified
information

Probabilistic Böhm Trees and Probabilistic Separation Thomas Leventis 
Probabilistic Böhm Trees and Probabilistic Separation Details 

Discussion Comments:
0
Verification:
Author has
not verified
information

Stochastic Shortest Paths and WeightBounded Properties in Markov Decision Processes Christel Baier, Nathalie Bertrand, Clemens Dubslaff, Daniel Gburek, Ocan Sankur 
Stochastic Shortest Paths and WeightBounded Properties in Markov Decision Processes Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

ModelTheoretic Characterization of Boolean and Arithmetic Circuit Classes of Small Depth Arnaud Durand, Anselm Haak, Heribert Vollmer 
ModelTheoretic Characterization of Boolean and Arithmetic Circuit Classes of Small Depth Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

A General Framework for Relational Parametricity Kristina Sojakova, Patricia Johann 
A General Framework for Relational Parametricity Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

The Geometry of ComputationGraph Abstraction Koko Muroya, Steven W. T. Cheung, Dan R. Ghica 
The Geometry of ComputationGraph Abstraction Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

A modal μ perspective on solving parity games in quasipolynomial time Karoliina Lehtinen 
A modal μ perspective on solving parity games in quasipolynomial time Details 

Discussion Comments:
0
Verification:
Author has
not verified
information

A sequent calculus with dependent types for classical arithmetic Étienne Miquey 
A sequent calculus with dependent types for classical arithmetic Details 

Discussion Comments:
0
Verification:
Author has
not verified
information

Regular Transducer Expressions for Regular Transformations Vrunda Dave, Paul Gastin, Shankara Narayanan Krishna 
Regular Transducer Expressions for Regular Transformations Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

A pseudoquasipolynomial algorithm for meanpayoff parity games Laure Daviaud, Marcin Jurdzinski, Ranko Lazic 
A pseudoquasipolynomial algorithm for meanpayoff parity games Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Black Ninjas in the Dark: Formal Analysis of Population Protocols Michael Blondin, Javier Esparza, Stefan Jaax, Antonín Kucera 
Black Ninjas in the Dark: Formal Analysis of Population Protocols Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Playing with Repetitions in Data Words Using Energy Games Diego Figueira, M. Praveen 
Playing with Repetitions in Data Words Using Energy Games Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Definable decompositions for graphs of bounded linear cliquewidth Mikolaj Bojanczyk, Martin Grohe, Michal Pilipczuk 
Definable decompositions for graphs of bounded linear cliquewidth Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Sound upto techniques and Complete abstract domains Filippo Bonchi, Pierre Ganty, Roberto Giacobazzi, Dusko Pavlovic 
Sound upto techniques and Complete abstract domains Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Rational Synthesis Under Imperfect Information Emmanuel Filiot, Raffaella Gentilini, JeanFrançois Raskin 
Rational Synthesis Under Imperfect Information Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

A Fixpoint Logic and Dependent Effects for Temporal Property Verification Yoji Nanjo, Hiroshi Unno, Eric Koskinen, Tachio Terauchi 
A Fixpoint Logic and Dependent Effects for Temporal Property Verification Details 
Discussion Comments:
0
Verification:
Authors have
not verified
information


The concurrent game semantics of Probabilistic PCF Simon Castellan, Pierre Clairambault, Hugo Paquet, Glynn Winskel 
The concurrent game semantics of Probabilistic PCF Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Work Analysis with ResourceAware Session Types Ankush Das, Jan Hoffmann, Frank Pfenning 
Work Analysis with ResourceAware Session Types Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

LMSO: A CurryHoward Approach to Church's Synthesis via Linear Logic Pierre Pradic, Colin Riba 
LMSO: A CurryHoward Approach to Church's Synthesis via Linear Logic Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Computable decision making on the reals and other spaces: via partiality and nondeterminism Benjamin Sherman, Luke Sciarappa, Adam Chlipala, Michael Carbin 
Computable decision making on the reals and other spaces: via partiality and nondeterminism Details 
Discussion Comments:
0
Verification:
Authors have
not verified
information


Sequential Relational Decomposition Dror Fried, Axel Legay, Joël Ouaknine, Moshe Y. Vardi 
Sequential Relational Decomposition Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

On the number of types in sparse graphs Michal Pilipczuk, Sebastian Siebertz, Szymon Torunczyk 
On the number of types in sparse graphs Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Syntax and Semantics of Quantitative Type Theory Robert Atkey 
Syntax and Semantics of Quantitative Type Theory Details 

Discussion Comments:
0
Verification:
Author has
not verified
information

Polynomial Invariants for Affine Programs Ehud Hrushovski, Joël Ouaknine, Amaury Pouly, James Worrell 
Polynomial Invariants for Affine Programs Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Continuous Reasoning: Scaling the impact of formal methods Peter W. O'Hearn 
Continuous Reasoning: Scaling the impact of formal methods Details 

Discussion Comments:
0
Verification:
Author has
not verified
information

Adrien Durier, Daniel Hirschkoff, Davide Sangiorgi 
Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Logical paradoxes in quantum computation Nadish de Silva 
Logical paradoxes in quantum computation Details 

Discussion Comments:
0
Verification:
Author has
not verified
information

A theory of linear typings as flows on 3valent graphs Noam Zeilberger 
A theory of linear typings as flows on 3valent graphs Details 
Discussion Comments:
0
Verification:
Author has
not verified
information


Wreath Products of Distributive Forest Algebras Michael Hahn, Andreas Krebs, Howard Straubing 
Wreath Products of Distributive Forest Algebras Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

An Asynchronous Soundness Theorem for Concurrent Separation Logic PaulAndré Melliès, Léo Stefanesco 
An Asynchronous Soundness Theorem for Concurrent Separation Logic Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

A parameterized halting problem, the linear time hierarchy, and the MRDP theorem Yijia Chen, Moritz Müller, Keita Yokoyama 
A parameterized halting problem, the linear time hierarchy, and the MRDP theorem Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Parameterized circuit complexity of modelchecking on sparse structures Michal Pilipczuk, Sebastian Siebertz, Szymon Torunczyk 
Parameterized circuit complexity of modelchecking on sparse structures Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Separability by piecewise testable languages and downward closures beyond subwords Georg Zetzsche 
Separability by piecewise testable languages and downward closures beyond subwords Details 

Discussion Comments:
0
Verification:
Author has
not verified
information

MSO Queries on Trees: Enumerating Answers under Updates Using Forest Algebras Matthias Niewerth 
MSO Queries on Trees: Enumerating Answers under Updates Using Forest Algebras Details 

Discussion Comments:
0
Verification:
Author has
not verified
information

Cellular Cohomology in Homotopy Type Theory Ulrik Buchholtz, KuenBang Hou (Favonia) 
Cellular Cohomology in Homotopy Type Theory Details 
Discussion Comments:
0
Verification:
Authors have
not verified
information


Treedepth, quantifier elimination, and quantifier rank Yijia Chen, Jörg Flum 
Treedepth, quantifier elimination, and quantifier rank Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Concurrency and Probability: Removing Confusion, Compositionally Roberto Bruni, Hernán C. Melgratti, Ugo Montanari 
Concurrency and Probability: Removing Confusion, Compositionally Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Higher Groups in Homotopy Type Theory Ulrik Buchholtz, Floris van Doorn, Egbert Rijke 
Higher Groups in Homotopy Type Theory Details 
Discussion Comments:
0
Verification:
Authors have
not verified
information


BooleanValued Semantics for the Stochastic λCalculus Giorgio Bacci, Robert Furber, Dexter Kozen, Radu Mardare, Prakash Panangaden, Dana Scott 
BooleanValued Semantics for the Stochastic λCalculus Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

On Higher Inductive Types in Cubical Type Theory Thierry Coquand, Simon Huber, Anders Mörtberg 
On Higher Inductive Types in Cubical Type Theory Details 
Discussion Comments:
0
Verification:
Authors have
not verified
information


Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types Valentin Blot, Jim Laird 
Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

A Logical Account for Linear Partial Differential Equations Marie Kerjean 
A Logical Account for Linear Partial Differential Equations Details 

Discussion Comments:
0
Verification:
Author has
not verified
information

A Simple and Optimal Complementation Algorithm for Büchi Automata Joël D. Allred, Ulrich UltesNitsche 
A Simple and Optimal Complementation Algorithm for Büchi Automata Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Andreas Nuyts, Dominique Devriese 
Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Regular and FirstOrder List Functions Mikolaj Bojanczyk, Laure Daviaud, Shankara Narayanan Krishna 
Regular and FirstOrder List Functions Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Karl Crary 
Details 
Discussion Comments:
0
Verification:
Author has
not verified
information


Differential Equation Axiomatization: The Impressive Power of Differential Ghosts André Platzer, Yong Kiam Tan 
Differential Equation Axiomatization: The Impressive Power of Differential Ghosts Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Neil Ghani, Jules Hedges, Viktor Winschel, Philipp Zahn 
Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Probabilistic Stable Functions on Discrete Cones are Power Series Raphaëlle Crubillé 
Probabilistic Stable Functions on Discrete Cones are Power Series Details 

Discussion Comments:
0
Verification:
Author has
not verified
information

A functional interpretation with state Thomas Powell 
A functional interpretation with state Details 

Discussion Comments:
0
Verification:
Author has
not verified
information

Every λTerm is Meaningful for the Infinitary Relational Model Pierre Vial 
Every λTerm is Meaningful for the Infinitary Relational Model Details 

Discussion Comments:
0
Verification:
Author has
not verified
information

Thomas Ferrère, Thomas A. Henzinger, N. Ege Saraç 
Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

AutomatonBased Criteria for Membership in CTL Udi Boker, Yariv Shaulian 
AutomatonBased Criteria for Membership in CTL Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Riesz Modal Logic with Threshold Operators Matteo Mio 
Riesz Modal Logic with Threshold Operators Details 

Discussion Comments:
0
Verification:
Author has
not verified
information

Two complete axiomatisations of purestate qubit quantum computing Amar Hadzihasanovic, Kang Feng Ng, Quanlong Wang 
Two complete axiomatisations of purestate qubit quantum computing Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

A van Benthem Theorem for Fuzzy Modal Logic Paul Wild, Lutz Schröder, Dirk Pattinson, Barbara König 
A van Benthem Theorem for Fuzzy Modal Logic Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Computability Beyond ChurchTuring via Choice Sequences Mark Bickford, Liron Cohen, Robert L. Constable, Vincent Rahli 
Computability Beyond ChurchTuring via Choice Sequences Details 
Discussion Comments:
0
Verification:
Authors have
not verified
information


A universalalgebraic proof of the complexity dichotomy for Monotone Monadic SNP Manuel Bodirsky, Florent R. Madelaine, Antoine Mottet 
A universalalgebraic proof of the complexity dichotomy for Monotone Monadic SNP Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

A Generalized Modality for Recursion Adrien Guatto 
A Generalized Modality for Recursion Details 

Discussion Comments:
0
Verification:
Author has
not verified
information

Impredicative Encodings of (Higher) Inductive Types Steve Awodey, Jonas Frey, Sam Speight 
Impredicative Encodings of (Higher) Inductive Types Details 
Discussion Comments:
0
Verification:
Authors have
not verified
information


Weighted model counting beyond twovariable logic Antti Kuusisto, Carsten Lutz 
Weighted model counting beyond twovariable logic Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Causal Computational Complexity of Distributed Processes Romain Demangeon, Nobuko Yoshida 
Causal Computational Complexity of Distributed Processes Details 
Discussion Comments:
0
Verification:
Authors have
not verified
information


Diagrammatic Reasoning beyond Clifford+T Quantum Mechanics Emmanuel Jeandel, Simon Perdrix, Renaud Vilmart 
Diagrammatic Reasoning beyond Clifford+T Quantum Mechanics Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, Fabio Zanasi 
Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

On computability and tractability for infinite sets Mikolaj Bojanczyk, Szymon Torunczyk 
On computability and tractability for infinite sets Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Logics for Word Transductions with Synthesis Luc Dartois, Emmanuel Filiot, Nathan Lhote 
Logics for Word Transductions with Synthesis Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Unification nets: canonical proof net quantifiers Dominic J. D. Hughes 
Unification nets: canonical proof net quantifiers Details 

Discussion Comments:
0
Verification:
Author has
not verified
information

Definable Ellipsoid Method, SumsofSquares Proofs, and the Isomorphism Problem Albert Atserias, Joanna Ochremiak 
Definable Ellipsoid Method, SumsofSquares Proofs, and the Isomorphism Problem Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

A Complete Axiomatisation of the ZXCalculus for Clifford+T Quantum Mechanics Emmanuel Jeandel, Simon Perdrix, Renaud Vilmart 
A Complete Axiomatisation of the ZXCalculus for Clifford+T Quantum Mechanics Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Typetwo polynomialtime and restricted lookahead Bruce M. Kapron, Florian Steinberg 
Typetwo polynomialtime and restricted lookahead Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Quantitative Behavioural Reasoning for Higherorder Effectful Programs: Applicative Distances Francesco Gavazzo 
Quantitative Behavioural Reasoning for Higherorder Effectful Programs: Applicative Distances Details 

Discussion Comments:
0
Verification:
Author has
not verified
information

A Hybrid, Dynamic Logic for HybridDynamic Information Flow Brandon Bohrer, André Platzer 
A Hybrid, Dynamic Logic for HybridDynamic Information Flow Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS Tomás Brázdil, Krishnendu Chatterjee, Antonín Kucera, Petr Novotný, Dominik Velan, Florian Zuleger 
Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Around Classical and Intuitionistic Linear Logics Olivier Laurent 
Around Classical and Intuitionistic Linear Logics Details 

Discussion Comments:
0
Verification:
Author has
not verified
information

What's in a game?: A theory of game models Clovis Eberhart, Tom Hirschowitz 
What's in a game?: A theory of game models Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Can One Escape Red Chains?: Regular Path Queries Determinacy is Undecidable Grzegorz Gluch, Jerzy Marcinkowski, Piotr OstropolskiNalewaja 
Can One Escape Red Chains?: Regular Path Queries Determinacy is Undecidable Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Enriching a Linear/Nonlinear Lambda Calculus: A Programming Language for String Diagrams Bert Lindenhovius, Michael Mislove, Vladimir Zamdzhiev 
Enriching a Linear/Nonlinear Lambda Calculus: A Programming Language for String Diagrams Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Takeshi Tsukada, Kazuyuki Asada, C.H. Luke Ong 
Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Syntax and Semantics for Operations with Scopes Maciej Piróg, Tom Schrijvers, Nicolas Wu, Mauro Jaskelioff 
Syntax and Semantics for Operations with Scopes Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Dialectica models of type theory Sean K. Moss, Tamara von Glehn 
Dialectica models of type theory Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

ReLoC: A Mechanised Relational Logic for FineGrained Concurrency Dan Frumin, Robbert Krebbers, Lars Birkedal 
ReLoC: A Mechanised Relational Logic for FineGrained Concurrency Details 
Discussion Comments:
0
Verification:
Authors have
not verified
information


Thierry Coquand 
Details 

Discussion Comments:
0
Verification:
Author has
not verified
information

Allegories: decidability and graph homomorphisms Damien Pous, Valeria Vignudelli 
Allegories: decidability and graph homomorphisms Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

An answer to the Gamma question Benoit Monin 
An answer to the Gamma question Details 

Discussion Comments:
0
Verification:
Author has
not verified
information

Guarded Computational Type Theory Jonathan Sterling, Robert Harper 
Guarded Computational Type Theory Details 
Discussion Comments:
0
Verification:
Authors have
not verified
information


Satisfiability in multivalued circuits Pawel M. Idziak, Jacek Krzaczkowski 
Satisfiability in multivalued circuits Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Classical realizability as a classifier for nondeterminism Guillaume Geoffroy 
Classical realizability as a classifier for nondeterminism Details 

Discussion Comments:
0
Verification:
Author has
not verified
information

QuasiOpen Bisimilarity with Mismatch is Intuitionistic Ross Horne, Ki Yung Ahn, ShangWei Lin, Alwen Tiu 
QuasiOpen Bisimilarity with Mismatch is Intuitionistic Details 
Discussion Comments:
0
Verification:
Authors have
not verified
information


Free Higher Groups in Homotopy Type Theory Nicolai Kraus, Thorsten Altenkirch 
Free Higher Groups in Homotopy Type Theory Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

Distributionbased objectives for Markov Decision Processes S. Akshay, Blaise Genest, Nikhil Vyas 
Distributionbased objectives for Markov Decision Processes Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information

PaulAndré Melliès 
Details 

Discussion Comments:
0
Verification:
Author has
not verified
information

Unary negation fragment with equivalence relations has the finite model property Daniel Danielski, Emanuel Kieronski 
Unary negation fragment with equivalence relations has the finite model property Details 

Discussion Comments:
0
Verification:
Authors have
not verified
information
