LICS '16- Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science

Full Citation in the ACM Digital Library

SESSION: Invited Presentations

Unifying Logical and Statistical AI

Duality in Computer Science

Blockchains and the Logic of Accountability: Keynote Address

The Probabilistic Model Checking Landscape

SESSION: Probabilistic Models of Computation

Stochastic mechanics of graph rewriting

On the Satisfiability of Some Simple Probabilistic Logics

Distinguishing Hidden Markov Chains

Quantitative Automata under Probabilistic Semantics

SESSION: Decidability

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

The Diagonal Problem for Higher-Order Recursion Schemes is Decidable

Two-variable Logic with a Between Relation

Decidability and Complexity for Quiescent Consistency

SESSION: Proof Theory

From positive and intuitionistic bounded arithmetic to monotone proof complexity

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

Understanding Gentzen and Frege Systems for QBF

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

SESSION: Model Checking

Data Communicating Processes with Unreliable Channels

A New Perspective on FO Model Checking of Dense Graph Classes

Proving Liveness of Parameterized Programs

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

SESSION: Automata Theory

The complexity of regular abstractions of one-counter languages

Two-Way Visibly Pushdown Automata and Transducers

Automata on Infinite Trees with Equality and Disequality Constraints Between Siblings

SESSION: Games and Logic

Plays as Resource Terms via Non-idempotent Intersection Types

Perfect-Information Stochastic Games with Generalized Mean-Payoff Objectives

Games with bound guess actions

SESSION: Model Theory

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

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

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

Querying Visible and Invisible Information

SESSION: Induction/Coinduction

Coinduction All the Way Up

Denotational semantics of recursive types in synthetic guarded domain theory

Type Theory based on Dependent Inductive and Coinductive Types

Program Equivalence is Coinductive

SESSION: Semantics

Fixed Points In Quantitative Semantics

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

The Definitional Side of the Forcing

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

SESSION: Monadic Second-Order Logic

First-order definability of rational transductions: An algebraic approach

Order Invariance on Decomposable Structures

Definability equals recognizability for graphs of bounded treewidth

Monadic second order logic as the model companion of temporal logic

SESSION: Linear Logic

Interaction Graphs: Full Linear Logic

Conflict nets: Efficient locally canonical MALL proof nets

Infinitary Lambda Calculi from a Linear Perspective

SESSION: Reachability

First-order logic with reachability for infinite-state systems

The Complexity of Coverability in ν-Petri Nets

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

SESSION: Hybrid Systems

Comparing Chemical Reaction Networks: A Categorical and Algorithmic Perspective

A categorical approach to open and interconnected dynamical systems

Differential Refinement Logic

On Recurrent Reachability for Continuous Linear Dynamical Systems

SESSION: Category Theory

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

Interacting Frobenius Algebras are Hopf

Semi-galois Categories I: The Classical Eilenberg Variety Theory

A bifibrational reconstruction of Lawvere's presheaf hyperdoctrine

SESSION: Type Theory

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

Hybrid realizability for intuitionistic and classical choice

Trace semantics for polymorphic references

Constructions with Non-Recursive Higher Inductive Types

A constructive function-theoretic approach to topological compactness

SESSION: Constraint Solving

The algebraic dichotomy conjecture for infinite domain Constraint Satisfaction Problems

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

Weak consistency notions for all the CSPs of bounded width

Graphs of relational structures: restricted types

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

SESSION: Kleene Award

Winning Cores in Parity Games

SESSION: Probabilistic Models of Computation

Reasoning about Recursive Probabilistic Programs

Healthiness from Duality

Kolmogorov Extension, Martingale Convergence, and Compositionality of Processes

Quantitative Algebraic Reasoning

SESSION: Algebraic Methods

Rewriting modulo symmetric monoidal structure

Effective Brenier Theorem: Applications to Computable Analysis and Algorithmic Randomness

Quantifier Free Definability on Infinite Algebras

Factor Varieties and Symbolic Computation

SESSION: Logics of Programs

Proving Differential Privacy via Probabilistic Couplings

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

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

Divide and Congruence II: Delay and Weak Bisimilarity

SESSION: Decidability

How unprovable is Rabin's decidability theorem?

Solvability of Matrix-Exponential Equations

Order-Invariance of Two-Variable Logic is Decidable

A Step Up in Expressiveness of Decidable Fixpoint Logics

SESSION: Complexity

Church Meets Cook and Levin

Complexity Theory of (Functions on) Compact Metric Spaces

Semantically Acyclic Conjunctive Queries under Functional Dependencies

SESSION: Automata Theory

A Generalised Twinning Property for Minimisation of Cost Register Automata

Invisible Pushdown Languages

Minimization of Symbolic Tree Automata