ACM/IEEE Logic in Computer Science, LICS 2016


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

Blockchains and the Logic of Accountability: Keynote Address

Maurice Herlihy, Mark Moir

Blockchains and the Logic of Accountability: Keynote Address

Details
Discussion Comments: 0
Verification: Authors have not verified information

Program Equivalence is Coinductive

Dirk Pattinson, Lutz Schröder

Program Equivalence is Coinductive

Details
Discussion Comments: 0
Verification: Authors have not verified information

A New Perspective on FO Model Checking of Dense Graph Classes

Jakub Gajarský, Petr Hlinený, Jan Obdrzálek, Daniel Lokshtanov, M. S. Ramanujan

A New Perspective on FO Model Checking of Dense Graph Classes

Details
Discussion Comments: 0
Verification: Authors have not verified information

Differential Refinement Logic

Sarah M. Loos, André Platzer

Differential Refinement Logic

Details
Discussion Comments: 0
Verification: Authors have not verified information

Proving Liveness of Parameterized Programs

Azadeh Farzan, Zachary Kincaid, Andreas Podelski

Proving Liveness of Parameterized Programs

Details
Discussion Comments: 0
Verification: Authors have not verified information

Hybrid realizability for intuitionistic and classical choice

Valentin Blot

Hybrid realizability for intuitionistic and classical choice

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

Infinitary Lambda Calculi from a Linear Perspective

Ugo Dal Lago

Infinitary Lambda Calculi from a Linear Perspective

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

Near-Optimal Lower Bounds on Quantifier Depth and Weisfeiler-Leman Refinement Steps

Christoph Berkholz, Jakob Nordström

Near-Optimal Lower Bounds on Quantifier Depth and Weisfeiler-Leman Refinement Steps

Details
Discussion Comments: 0
Verification: Authors have not verified information

First-order logic with reachability for infinite-state systems

Emanuele D'Osualdo, Roland Meyer, Georg Zetzsche

First-order logic with reachability for infinite-state systems

Details
Discussion Comments: 0
Verification: Authors have not verified information

Plays as Resource Terms via Non-idempotent Intersection Types

Takeshi Tsukada, C.-H. Luke Ong

Plays as Resource Terms via Non-idempotent Intersection Types

Details
Discussion Comments: 0
Verification: Authors have not verified information

Kolmogorov Extension, Martingale Convergence, and Compositionality of Processes

Dexter Kozen

Kolmogorov Extension, Martingale Convergence, and Compositionality of Processes

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

The Probabilistic Model Checking Landscape

Joost-Pieter Katoen

The Probabilistic Model Checking Landscape

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

Graphs of relational structures: restricted types

Andrei A. Bulatov

Graphs of relational structures: restricted types

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

Conflict nets: Efficient locally canonical MALL proof nets

Dominic J. D. Hughes, Willem Heijltjes

Conflict nets: Efficient locally canonical MALL proof nets

Details
Discussion Comments: 0
Verification: Authors have not verified information

The Diagonal Problem for Higher-Order Recursion Schemes is Decidable

Lorenzo Clemente, Pawel Parys, Sylvain Salvati, Igor Walukiewicz

The Diagonal Problem for Higher-Order Recursion Schemes is Decidable

Details
Discussion Comments: 0
Verification: Authors have not verified information

On the Satisfiability of Some Simple Probabilistic Logics

Souymodip Chakraborty, Joost-Pieter Katoen

On the Satisfiability of Some Simple Probabilistic Logics

Details
Discussion Comments: 0
Verification: Authors have not verified information

The algebraic dichotomy conjecture for infinite domain Constraint Satisfaction Problems

Libor Barto, Michael Pinsker

The algebraic dichotomy conjecture for infinite domain Constraint Satisfaction Problems

Details
Discussion Comments: 0
Verification: Authors have not verified information

A Generalised Twinning Property for Minimisation of Cost Register Automata

Laure Daviaud, Pierre-Alain Reynier, Jean-Marc Talbot

A Generalised Twinning Property for Minimisation of Cost Register Automata

Details
Discussion Comments: 0
Verification: Authors have not verified information

Factor Varieties and Symbolic Computation

Antonino Salibra, Giulio Manzonetto, Giordano Favro

Factor Varieties and Symbolic Computation

Details
Discussion Comments: 0
Verification: Authors have not verified information

Comparing Chemical Reaction Networks: A Categorical and Algorithmic Perspective

Luca Cardelli, Mirco Tribastone, Max Tschaikowski, Andrea Vandin

Comparing Chemical Reaction Networks: A Categorical and Algorithmic Perspective

Details
Discussion Comments: 0
Verification: Authors have not verified information

Proving Differential Privacy via Probabilistic Couplings

Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub

Proving Differential Privacy via Probabilistic Couplings

Details
Discussion Comments: 0
Verification: Authors have not verified information

The Definitional Side of the Forcing

Guilhem Jaber, Gabriel Lewertowski, Pierre-Marie Pédrot, Matthieu Sozeau, Nicolas Tabareau

The Definitional Side of the Forcing

Details
Discussion Comments: 0
Verification: Authors have not verified information

Complexity Theory of (Functions on) Compact Metric Spaces

Akitoshi Kawamura, Florian Steinberg, Martin Ziegler

Complexity Theory of (Functions on) Compact Metric Spaces

Details
Discussion Comments: 0
Verification: Authors have not verified information

First-order definability of rational transductions: An algebraic approach

Emmanuel Filiot, Olivier Gauwin, Nathan Lhote

First-order definability of rational transductions: An algebraic approach

Details
Discussion Comments: 0
Verification: Authors have not verified information

Reasoning about Recursive Probabilistic Programs

Federico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja

Reasoning about Recursive Probabilistic Programs

Details
Author Comments:
Discussion Comments: 0
Sharing: Research produced no artifacts
Verification: Authors have verified information

Two-variable Logic with a Between Relation

Andreas Krebs, Kamal Lodaya, Paritosh K. Pandya, Howard Straubing

Two-variable Logic with a Between Relation

Details
Discussion Comments: 0
Verification: Authors have not verified information

Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints

Sam Staton, Hongseok Yang, Frank Wood, Chris Heunen, Ohad Kammar

Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints

Details
Discussion Comments: 0
Verification: Authors have not verified information

The complexity of regular abstractions of one-counter languages

Mohamed Faouzi Atig, Dmitry Chistikov, Piotr Hofman, K. Narayan Kumar, Prakash Saivasan, Georg Zetzsche

The complexity of regular abstractions of one-counter languages

Details
Discussion Comments: 0
Verification: Authors have not verified information

Order Invariance on Decomposable Structures

Michael Elberfeld, Marlin Frickenschmidt, Martin Grohe

Order Invariance on Decomposable Structures

Details
Discussion Comments: 0
Verification: Authors have not verified information

Solvability of Matrix-Exponential Equations

Joël Ouaknine, Amaury Pouly, João Sousa Pinto, James Worrell

Solvability of Matrix-Exponential Equations

Details
Discussion Comments: 0
Verification: Authors have not verified information

Decidability and Complexity for Quiescent Consistency

Brijesh Dongol, Robert M. Hierons

Decidability and Complexity for Quiescent Consistency

Details
Discussion Comments: 0
Verification: Authors have not verified information

Understanding Gentzen and Frege Systems for QBF

Olaf Beyersdorff, Ján Pich

Understanding Gentzen and Frege Systems for QBF

Details
Discussion Comments: 0
Verification: Authors have not verified information

Divide and Congruence II: Delay and Weak Bisimilarity

Wan Fokkink, Rob J. van Glabbeek

Divide and Congruence II: Delay and Weak Bisimilarity

Details
Discussion Comments: 0
Verification: Authors have not verified information

Hanf normal form for first-order logic with unary counting quantifiers

Lucas Heimberg, Dietrich Kuske, Nicole Schweikardt

Hanf normal form for first-order logic with unary counting quantifiers

Details
Discussion Comments: 0
Verification: Authors have not verified information

Healthiness from Duality

Wataru Hino, Hiroki Kobayashi, Ichiro Hasuo, Bart Jacobs

Healthiness from Duality

Details
Discussion Comments: 0
Verification: Authors have not verified information

Semantically Acyclic Conjunctive Queries under Functional Dependencies

Diego Figueira

Semantically Acyclic Conjunctive Queries under Functional Dependencies

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

Winning Cores in Parity Games

Steen Vester

Winning Cores in Parity Games

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

Data Communicating Processes with Unreliable Channels

Parosh Aziz Abdulla, C. Aiswarya, Mohamed Faouzi Atig

Data Communicating Processes with Unreliable Channels

Details
Discussion Comments: 0
Verification: Authors have not verified information

Two-Way Visibly Pushdown Automata and Transducers

Luc Dartois, Emmanuel Filiot, Pierre-Alain Reynier, Jean-Marc Talbot

Two-Way Visibly Pushdown Automata and Transducers

Details
Discussion Comments: 0
Verification: Authors have not verified information

Perfect-Information Stochastic Games with Generalized Mean-Payoff Objectives

Krishnendu Chatterjee, Laurent Doyen

Perfect-Information Stochastic Games with Generalized Mean-Payoff Objectives

Details
Discussion Comments: 0
Verification: Authors have not verified information

Quantifier Free Definability on Infinite Algebras

Bakh Khoussainov

Quantifier Free Definability on Infinite Algebras

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

The Complexity of Coverability in ν-Petri Nets

Ranko Lazic, Sylvain Schmitz

The Complexity of Coverability in ν-Petri Nets

Details
Discussion Comments: 0
Verification: Authors have not verified information

Type Theory based on Dependent Inductive and Coinductive Types

Henning Basold, Herman Geuvers

Type Theory based on Dependent Inductive and Coinductive Types

Details
Discussion Comments: 0
Verification: Authors have not verified information

Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-Complete

Matthias Englert, Ranko Lazic, Patrick Totzke

Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-Complete

Details
Discussion Comments: 0
Verification: Authors have not verified information

Towards Compositional Feedback in Non-Deterministic and Non-Input-Receptive Systems

Viorel Preoteasa, Stavros Tripakis

Towards Compositional Feedback in Non-Deterministic and Non-Input-Receptive Systems

Details
Discussion Comments: 0
Verification: Authors have not verified information

Deciding First-Order Satisfiability when Universal and Existential Variables are Separated

Thomas Sturm, Marco Voigt, Christoph Weidenbach

Deciding First-Order Satisfiability when Universal and Existential Variables are Separated

Details
Discussion Comments: 0
Verification: Authors have not verified information

Denotational semantics of recursive types in synthetic guarded domain theory

Rasmus Ejlers Møgelberg, Marco Paviotti

Denotational semantics of recursive types in synthetic guarded domain theory

Details
Discussion Comments: 0
Verification: Authors have not verified information

Automata on Infinite Trees with Equality and Disequality Constraints Between Siblings

Arnaud Carayol, Christof Löding, Olivier Serre

Automata on Infinite Trees with Equality and Disequality Constraints Between Siblings

Details
Discussion Comments: 0
Verification: Authors have not verified information

On Recurrent Reachability for Continuous Linear Dynamical Systems

Ventsislav Chonev, Joël Ouaknine, James Worrell

On Recurrent Reachability for Continuous Linear Dynamical Systems

Details
Discussion Comments: 0
Verification: Authors have not verified information

Effective Brenier Theorem: Applications to Computable Analysis and Algorithmic Randomness

Alex Galicki

Effective Brenier Theorem: Applications to Computable Analysis and Algorithmic Randomness

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

A Step Up in Expressiveness of Decidable Fixpoint Logics

Michael Benedikt, Pierre Bourhis, Michael Vanden Boom

A Step Up in Expressiveness of Decidable Fixpoint Logics

Details
Discussion Comments: 0
Verification: Authors have not verified information

Trace semantics for polymorphic references

Guilhem Jaber, Nikos Tzevelekos

Trace semantics for polymorphic references

Details
Discussion Comments: 0
Verification: Authors have not verified information

From positive and intuitionistic bounded arithmetic to monotone proof complexity

Anupam Das

From positive and intuitionistic bounded arithmetic to monotone proof complexity

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

Duality in Computer Science

Mai Gehrke

Duality in Computer Science

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

How unprovable is Rabin's decidability theorem?

Leszek Aleksander Kolodziejczyk, Henryk Michalewski

How unprovable is Rabin's decidability theorem?

Details
Discussion Comments: 0
Verification: Authors have not verified information

Weak consistency notions for all the CSPs of bounded width

Marcin Kozik

Weak consistency notions for all the CSPs of bounded width

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

Gödel's functional interpretation and the concept of learning

Thomas Powell

Gödel's functional interpretation and the concept of learning

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

Invisible Pushdown Languages

Eryk Kopczynski

Invisible Pushdown Languages

Details
Author Comments: A computer program was used to find the right words for one of the proofs, but I do not think it is of public interest (the proof works on its own) -- but if you are interested, please contact me.
Discussion Comments: 0
Sharing: Research produced no artifacts
Verification: Author has verified information

Querying Visible and Invisible Information

Michael Benedikt, Pierre Bourhis, Balder ten Cate, Gabriele Puppis

Querying Visible and Invisible Information

Details
Discussion Comments: 0
Verification: Authors have not verified information

Distinguishing Hidden Markov Chains

Stefan Kiefer, A. Prasad Sistla

Distinguishing Hidden Markov Chains

Details
Discussion Comments: 0
Verification: Authors have not verified information

Ability to Count Messages Is Worth Θ(Δ) Rounds in Distributed Computing

Tuomo Lempiäinen

Ability to Count Messages Is Worth Θ(Δ) Rounds in Distributed Computing

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

Model and Objective Separation with Conditional Lower Bounds: Disjunction is Harder than Conjunction

Krishnendu Chatterjee, Wolfgang Dvorák, Monika Henzinger, Veronika Loitzenbauer

Model and Objective Separation with Conditional Lower Bounds: Disjunction is Harder than Conjunction

Details
Discussion Comments: 0
Verification: Authors have not verified information

A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory

Kuen-Bang Hou (Favonia), Eric Finster, Daniel R. Licata, Peter LeFanu Lumsdaine

A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory

Details
Discussion Comments: 0
Verification: Authors have not verified information

The Power of Arc Consistency for CSPs Defined by Partially-Ordered Forbidden Patterns

Martin C. Cooper, Stanislav Zivny

The Power of Arc Consistency for CSPs Defined by Partially-Ordered Forbidden Patterns

Details
Discussion Comments: 0
Verification: Authors have not verified information

Stochastic mechanics of graph rewriting

Nicolas Behr, Vincent Danos, Ilias Garnier

Stochastic mechanics of graph rewriting

Details
Discussion Comments: 0
Verification: Authors have not verified information

Constructions with Non-Recursive Higher Inductive Types

Nicolai Kraus

Constructions with Non-Recursive Higher Inductive Types

Details
Author Comments:
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Author has verified information

Fixed Points In Quantitative Semantics

J. Laird

Fixed Points In Quantitative Semantics

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

Rewriting modulo symmetric monoidal structure

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

Rewriting modulo symmetric monoidal structure

Details
Discussion Comments: 0
Verification: Authors have not verified information

Monadic second order logic as the model companion of temporal logic

Silvio Ghilardi, Sam van Gool

Monadic second order logic as the model companion of temporal logic

Details
Discussion Comments: 0
Verification: Authors have not verified information

Definability equals recognizability for graphs of bounded treewidth

Mikolaj Bojanczyk, Michal Pilipczuk

Definability equals recognizability for graphs of bounded treewidth

Details
Discussion Comments: 0
Verification: Authors have not verified information

Interaction Graphs: Full Linear Logic

Thomas Seiller

Interaction Graphs: Full Linear Logic

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

Games with bound guess actions

Thomas Colcombet, Stefan Göller

Games with bound guess actions

Details
Discussion Comments: 0
Verification: Authors have not verified information

Quantitative Algebraic Reasoning

Radu Mardare, Prakash Panangaden, Gordon D. Plotkin

Quantitative Algebraic Reasoning

Details
Discussion Comments: 0
Verification: Authors have not verified information

Order-Invariance of Two-Variable Logic is Decidable

Thomas Zeume, Frederik Harwath

Order-Invariance of Two-Variable Logic is Decidable

Details
Discussion Comments: 0
Verification: Authors have not verified information

Unified Semantics and Proof System for Classical, Intuitionistic and Affine Logics

Chuck Liang

Unified Semantics and Proof System for Classical, Intuitionistic and Affine Logics

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

Interacting Frobenius Algebras are Hopf

Ross Duncan, Kevin Dunne

Interacting Frobenius Algebras are Hopf

Details
Discussion Comments: 0
Verification: Authors have not verified information

Upper Bounds on the Quantifier Depth for Graph Differentiation in First Order Logic

Sandra Kiefer, Pascal Schweitzer

Upper Bounds on the Quantifier Depth for Graph Differentiation in First Order Logic

Details
Discussion Comments: 0
Verification: Authors have not verified information

Towards Completeness via Proof Search in the Linear Time μ-calculus: The case of Büchi inclusions

Amina Doumane, David Baelde, Lucca Hirschi, Alexis Saurin

Towards Completeness via Proof Search in the Linear Time μ-calculus: The case of Büchi inclusions

Details
Discussion Comments: 0
Verification: Authors have not verified information

Coinduction All the Way Up

Damien Pous

Coinduction All the Way Up

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

Unifying Logical and Statistical AI

Pedro M. Domingos, Daniel Lowd, Stanley Kok, Aniruddh Nath, Hoifung Poon, Matthew Richardson, Parag Singla

Unifying Logical and Statistical AI

Details
Discussion Comments: 0
Verification: Authors have not verified information

A categorical approach to open and interconnected dynamical systems

Brendan Fong, Pawel Sobocinski, Paolo Rapisarda

A categorical approach to open and interconnected dynamical systems

Details
Discussion Comments: 0
Verification: Authors have not verified information

Church Meets Cook and Levin

Damiano Mazza

Church Meets Cook and Levin

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

Quantitative Automata under Probabilistic Semantics

Krishnendu Chatterjee, Thomas A. Henzinger, Jan Otop

Quantitative Automata under Probabilistic Semantics

Details
Discussion Comments: 0
Verification: Authors have not verified information

Minimization of Symbolic Tree Automata

Loris D'Antoni, Margus Veanes

Minimization of Symbolic Tree Automata

Details
Discussion Comments: 0
Verification: Authors have not verified information

On Thin Air Reads Towards an Event Structures Model of Relaxed Memory

Alan Jeffrey, James Riely

On Thin Air Reads Towards an Event Structures Model of Relaxed Memory

Details
Discussion Comments: 0
Verification: Authors have not verified information

A constructive function-theoretic approach to topological compactness

Iosif Petrakis

A constructive function-theoretic approach to topological compactness

Details
Author Comments:
Discussion Comments: 0
Sharing: Research produced no artifacts
Verification: Author has verified information

A bifibrational reconstruction of Lawvere's presheaf hyperdoctrine

Paul-André Melliès, Noam Zeilberger

A bifibrational reconstruction of Lawvere's presheaf hyperdoctrine

Details
Discussion Comments: 0
Verification: Authors have not verified information

Reducts of finitely bounded homogeneous structures, and lifting tractability from finite-domain constraint satisfaction

Manuel Bodirsky, Antoine Mottet

Reducts of finitely bounded homogeneous structures, and lifting tractability from finite-domain constraint satisfaction

Details
Discussion Comments: 0
Verification: Authors have not verified information

Semi-galois Categories I: The Classical Eilenberg Variety Theory

Takeo Uramoto

Semi-galois Categories I: The Classical Eilenberg Variety Theory

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