| Title/Authors | Title | Research Artifacts
[?] A research
artifact is any by-product 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, shell-scripts 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 Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes Jan Kretínský, Tobias Meggendorfer |
Conditional Value-at-Risk 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 Weight-Bounded Properties in Markov Decision Processes Christel Baier, Nathalie Bertrand, Clemens Dubslaff, Daniel Gburek, Ocan Sankur |
Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Model-Theoretic Characterization of Boolean and Arithmetic Circuit Classes of Small Depth Arnaud Durand, Anselm Haak, Heribert Vollmer |
Model-Theoretic 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 |
|
Author Comments:
none
Discussion Comments:
0
Sharing:
Research produced no artifacts
Verification:
Authors have
verified
information
|
|
The Geometry of Computation-Graph Abstraction Koko Muroya, Steven W. T. Cheung, Dan R. Ghica |
The Geometry of Computation-Graph Abstraction Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
A modal μ perspective on solving parity games in quasi-polynomial time Karoliina Lehtinen |
A modal μ perspective on solving parity games in quasi-polynomial 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 pseudo-quasi-polynomial algorithm for mean-payoff parity games Laure Daviaud, Marcin Jurdzinski, Ranko Lazic |
A pseudo-quasi-polynomial algorithm for mean-payoff 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 |
|
Author Comments:
Discussion Comments:
0
Sharing:
Research produced no artifacts
Verification:
Authors have
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 up-to techniques and Complete abstract domains Filippo Bonchi, Pierre Ganty, Roberto Giacobazzi, Dusko Pavlovic |
Sound up-to techniques and Complete abstract domains Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Rational Synthesis Under Imperfect Information Emmanuel Filiot, Raffaella Gentilini, Jean-Franç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 Resource-Aware Session Types Ankush Das, Jan Hoffmann, Frank Pfenning |
Work Analysis with Resource-Aware Session Types Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic Pierre Pradic, Colin Riba |
LMSO: A Curry-Howard 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 |
Author Comments:
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
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 3-valent graphs Noam Zeilberger |
A theory of linear typings as flows on 3-valent 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 Paul-André 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 model-checking on sparse structures Michal Pilipczuk, Sebastian Siebertz, Szymon Torunczyk |
Parameterized circuit complexity of model-checking 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, Kuen-Bang Hou (Favonia) |
Cellular Cohomology in Homotopy Type Theory Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Tree-depth, quantifier elimination, and quantifier rank Yijia Chen, Jörg Flum |
Tree-depth, 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
|
|
|
Boolean-Valued Semantics for the Stochastic λ-Calculus Giorgio Bacci, Robert Furber, Dexter Kozen, Radu Mardare, Prakash Panangaden, Dana S. Scott |
Boolean-Valued 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 Ultes-Nitsche |
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 |
|
Author Comments:
This paper comes with a technical report containing technical details and non-mechanized proofs: https://arxiv.org/abs/1805.08684
Discussion Comments:
0
Sharing:
Research produced no artifacts
Verification:
Authors have
verified
information
|
|
Regular and First-Order List Functions Mikolaj Bojanczyk, Laure Daviaud, Shankara Narayanan Krishna |
Regular and First-Order 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
|
|
Automaton-Based Criteria for Membership in CTL Udi Boker, Yariv Shaulian |
Automaton-Based 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 pure-state qubit quantum computing Amar Hadzihasanovic, Kang Feng Ng, Quanlong Wang |
Two complete axiomatisations of pure-state qubit quantum computing Details |
|
Author Comments:
Discussion Comments:
0
Sharing:
Research produced no artifacts
Verification:
Authors have
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 |
|
Author Comments:
Discussion Comments:
0
Sharing:
Research produced no artifacts
Verification:
Authors have
verified
information
|
|
Computability Beyond Church-Turing via Choice Sequences Mark Bickford, Liron Cohen, Robert L. Constable, Vincent Rahli |
Computability Beyond Church-Turing via Choice Sequences Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP Manuel Bodirsky, Florent R. Madelaine, Antoine Mottet |
A universal-algebraic 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 two-variable logic Antti Kuusisto, Carsten Lutz |
Weighted model counting beyond two-variable 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, Sums-of-Squares Proofs, and the Isomorphism Problem Albert Atserias, Joanna Ochremiak |
Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism Problem Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics Emmanuel Jeandel, Simon Perdrix, Renaud Vilmart |
A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Type-two polynomial-time and restricted lookahead Bruce M. Kapron, Florian Steinberg |
Type-two polynomial-time and restricted lookahead Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances Francesco Gavazzo |
Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances Details |
|
Discussion Comments:
0
Verification:
Author has
not verified
information
|
|
A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow Brandon Bohrer, André Platzer |
A Hybrid, Dynamic Logic for Hybrid-Dynamic 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 |
|
Author Comments:
Discussion Comments:
0
Sharing:
Research produced no artifacts
Verification:
Authors have
verified
information
|
|
Can One Escape Red Chains?: Regular Path Queries Determinacy is Undecidable Grzegorz Gluch, Jerzy Marcinkowski, Piotr Ostropolski-Nalewaja |
Can One Escape Red Chains?: Regular Path Queries Determinacy is Undecidable Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams Bert Lindenhovius, Michael W. Mislove, Vladimir Zamdzhiev |
Enriching a Linear/Non-linear 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 Fine-Grained Concurrency Dan Frumin, Robbert Krebbers, Lars Birkedal |
ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency Details |
Author Comments:
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
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 |
Author Comments:
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
|
Satisfiability in multi-valued circuits Pawel M. Idziak, Jacek Krzaczkowski |
Satisfiability in multi-valued 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
|
|
Quasi-Open Bisimilarity with Mismatch is Intuitionistic Ross Horne, Ki Yung Ahn, Shang-Wei Lin, Alwen Tiu |
Quasi-Open 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
|
|
Distribution-based objectives for Markov Decision Processes S. Akshay, Blaise Genest, Nikhil Vyas |
Distribution-based objectives for Markov Decision Processes Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Paul-André 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
|