LICS 2017 Accepted Papers

Piotr Hofman, Jérôme Leroux and Patrick Totzke. Linear Combinations of Unordered Data Vectors
Valentin Blot. An interpretation of system F through bar recursion
Mathieu Hoyrup and Walid Gomaa. On the extension of computable real functions
Michael Blondin and Christoph Haase. Logics for Continuous Reachability in Petri Nets and Vector Addition Systems with States
Gérard Cécé. Foundation for a Series of Efficient Simulation Algorithms
Thomas Place and Marc Zeitoun. Separation for Dot-Depth Two
Jasmin Christian Blanchette, Fabian Meier, Andrei Popescu and Dmitriy Traytel. Foundational Nonuniform (Co)datatypes for Higher-Order Logic
Felix Canavoi and Martin Otto. Common Knowledge and Multi-Scale Locality Analysis in Cayley Structures
Simone Bova and Fabio Mogavero. Herbrand Property: Finite Quasi-Herbrand Models and Lifting Chandra-Merlin Theorem to Quantified Conjunctive Queries
Vincent Rahli, Mark Bickford and Robert Constable. Bar Induction: The Good, the Bad, and the Ugly
Amina Doumane. Constructive completeness for the linear-time mu-calculus
Federico Aschieri, Agata Ciabattoni and Francesco Genco. Gödel Logic: From Natural Deduction to Parallel Computation
Paul-André Melliès. Higher-order parity automata
Bakh Khoussainov and Toru Takisaka. Large scale geometries of infinite strings
Wojciech Czerwiński and Sławomir Lasota. Regular Separability of One Counter Automata
Martin Grohe and Martin Ritzert. Learning first-order definable concepts over structures of small degree
Martin Grohe and Wied Pakusa. The Descriptive Complexity of Solving Linear Equation Systems and its Applications
Faried Abu Zaid, Anuj Dawar, Erich Grädel and Wied Pakusa. Definability of Summation Problems for Abelian Groups and Semigroups
Lorenzo Clemente, Slawomir Lasota, Ranko Lazic and Filip Mazowiecki. Timed pushdown automata and branching vector addition systems
Taichi Uemura. Fibred Fibration Categories
Hubie Chen and Stefan Mengel. The Logic of Counting Query Answers
Emmanuel Jeandel. Enumeration Reducibility in Closure Spaces with Applications to Logic and Algebra
Johan Thapper and Stanislav Živný. The Limits of SDP Relaxations for General-Valued CSPs
Bahareh Afshari and Graham Leigh. Cut-free Completeness for Modal Mu-Calculus
G. A. Kavvos. Dual-Context Calculi for Modal Logic
Christoph Haase, Stefan Kiefer and Markus Lohrey. Computing Quantiles in Markov Chains with Multi-Dimensional Costs
Matteo Mio, Robert Furber and Radu Mardare. Riesz Modal Logic for Markov Processes
Marcin Jurdzinski and Ranko Lazic. Succinct progress measures for solving parity games
Takeshi Tsukada, Kazuyuki Asada and Luke Ong. Generalised Species of Rigid Resource Terms
Marco Voigt. A fine-grained hierarchy of hard problems in the separated fragment
Aleks Kissinger and Sander Uijlen. A categorical semantics for causal structure
Emmanuel Filiot, Ismaël Jecker, Nathan Lhote, Guillermo Perez and Jean-Francois Raskin. On Delay and Regret Determinization of Max-Plus Automata
Patrick Bahr, Hans Bugge Grathwohl and Rasmus Ejlers Møgelberg. The Clocks Are Ticking: No More Delays! Reduction Semantics for Type Theory with Guarded Recursion
Karin Quaas, Mahsa Shirmohammadi and James Worrell. Revisiting Reachability in Timed Automata
Iddo Tzameret and Stephen Cook. Uniform, Integral and Efficient Proofs for the Determinant Identities
Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi and Dominik Wojtczak. Parity Objectives in Countable MDPs
Michael Benedikt, Timothy Duff, Aditya Sharad and James Worrell. Polynomial Automata: Zeroness and Applications
Radu Mardare, Prakash Panangaden and Gordon Plotkin. On Axiomatizability of the Quantitative Algebras
Pierre Vial. Infinitary Intersection Types as Sequences: a New Answer to Klop’s Problem
André Hernich and Phokion Kolaitis. Foundations of Information Integration under Bag Semantics
Thomas Colcombet, Marcin Jurdzinski, Ranko Lazic and Sylvain Schmitz. Perfect Half Space Games
Miguel Romero Orth, Pablo Barceló and Moshe Vardi. The Homomorphism Problem for Regular Graph Patterns
Sandra Kiefer, Ilia Ponomarenko and Pascal Schweitzer. The Weisfeiler-Leman dimension of planar graphs is at most 3
Anuj Dawar and Pengming Wang. Definability of Semidefinite Programming and Lasserre Lower Bounds for CSPs
Ohad Kammar, Paul Blain Levy, Sean Moss and Sam Staton. A monad for full ground reference cells
Dusko Pavlovic and Peter-Michael Seidel. Quotients in monadic programming: Projective algebras are equivalent to coalgebras
Yu-Fang Chen, Ondrej Lengal, Tony Tan and Zhilin Wu. Register automata with linear arithmetic
Ugo Dal Lago, Ryo Tanaka and Akira Yoshimizu. The Geometry of Concurrent Interaction: Handling Multiple Ports by Way of Multiple Tokens
Pierre-Marie Pédrot and Nicolas Tabareau. An Effectful Way to Eliminate Addiction to Dependence
Stefano Berardi and Makoto Tatsuta. Equivalence of Inductive Definitions and Cyclic Proofs under Arithmetic
Jan van den Heuvel, Stephan Kreutzer, Michał Pilipczuk, Roman Rabinovich, Sebastian Siebertz and Daniel A. Quiroz. Model-checking for successor-invariant first-order formulas on graph classes of bounded expansion
Michał Wrona. The Complexity of Minimal Inference Problem for Conservative Constraint Languages
Ugo Dal Lago, Francesco Gavazzo and Paul Blain Levy. Effectful Applicative Bisimilarity: Monads, Relators, and the Howe's Method
Malgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk, Damien Pous and Alan Schmitt. Fully Abstract Encodings of lambda-Calculus in HOcore through Abstract Machines
Venanzio Capretta and Jonathan Fowler. The Continuity of Monadic Stream Functions
Martin Hofmann and Jérémy Ledent. A cartesian closed category for higher-order model checking
Florent Capelli. Understanding the complexity of #SAT using knowledge compilation
Dimitri Surinx, Jan Van den Bussche and Dirk Van Gucht. The primitivity of operators in the algebra of binary relations under conjunctions of containments
Berit Grußien. Capturing Polynomial Time using Modular Decomposition
Eric Finster and Samuel Mimram. A Type-Theoretical Definition of Weak omega-Categories
Martin Zimmermann. Games with Costs and Delays
Rohit Chadha, A. Prasad Sistla and Mahesh Viswanathan. Verification of randomized security protocols
Andrej Dudenhefner and Jakob Rehof. Typability in Bounded Dimension
Libor Barto, Michael Kompatscher, Miroslav Olsak, Trung Van Pham and Michael Pinsker. The Two Dichotomy Conjectures for Infinite Domain Constraint Satisfaction Problems Are Equivalent
Samson Abramsky, Anuj Dawar and Pengming Wang. The Pebbling Comonad in Finite Model Theory
Thierry Coquand, Bassel Mannaa and Fabian Ruch. Stack Semantics of Type Theory
Richard Mayr, Sven Schewe, Patrick Totzke and Dominik Wojtczak. MDPs with Energy-Parity Objectives
Yoshiki Nakamura. Partial Derivatives on Graphs for Kleene Allegories
Dietrich Kuske and Nicole Schweikardt. First-order logic with counting: At least, WEAK Hanf normal forms always exist and can be computed!
Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi and Dominik Wojtczak. On Strong Determinacy of Countable Stochastic Games
Paolo Baldan, Andrea Corradini and Fabio Gadducci. Domains and Event Structures for Fusions
Raphaël Berthon, Bastien Maubert, Aniello Murano, Sasha Rubin and Moshe Vardi. Strategy Logic with Imperfect Information
Chris Heunen, Ohad Kammar, Sam Staton and Hongseok Yang. A Convenient Category for Higher-Order Probability Theory
Félix Baschenis, Olivier Gauwin, Anca Muscholl and Gabriele Puppis. Untwisting two-way transducers in elementary time
Florian Steinberg and Matthias Schröder. Bounded time computation on metric spaces and Banach spaces
Mai Gehrke, Daniela Petrisan and Luca Reggio. Quantifiers on languages and codensity monads
Simon Halfon, Philippe Schnoebelen and Georg Zetzsche. Decidability, complexity, and expressiveness of first-order logic over the subword ordering
Rob van Glabbeek. Lean and Full Congruence Formats for Recursion
Abbas Edalat and Mehrdad Maleki. Differentiation in Logical Form
Javier Esparza, Anca Muscholl and Igor Walukiewicz. Static Analysis of Deterministic Negotiations
Julien Cervelle and Gregory Lafitte. On shift-invariant maximal filters and hormonal cellular automata
Ulrik Buchholtz and Egbert Rijke. The real projective spaces in homotopy type theory
Krzysztof Bar and Jamie Vicary. Data structures for quasistrict higher categories
Michaël Cadilhac and Charles Paperman. A Crevice on the Crane Beach: Finite-Degree Predicates
Andrei Bulatov. Constraint Satisfaction Problems over semilattice block Mal'tsev algebras
Marcelo Arenas, Martín Muñoz and Cristian Riveros. Descriptive Complexity for Counting Complexity Classes
Suguman Bansal, Swarat Chaudhuri and Moshe Y. Vardi. Comparator automata in quantitative verification
Natsuki Urabe, Masaki Hara and Ichiro Hasuo. Categorical Liveness Checking by Corecursive Algebras
Robert Furber, Dexter Kozen, Kim Larsen, Radu Mardare and Prakash Panangaden. Unrestricted Stone Duality for Markov Processes
Benjamin Kaminski and Joost-Pieter Katoen. A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations