The Community for Technology Leaders
2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (2017)
Reykjavik, Iceland
June 20, 2017 to June 23, 2017
ISBN: 978-1-5090-3019-4
TABLE OF CONTENTS

Front title (PDF)

pp. c1

LICS 2017 foreword (PDF)

Joel Ouaknine , MPI-SWS & University of Oxford, UK
pp. ii-iv

Committees (PDF)

pp. v-vi

External reviewers (PDF)

pp. vii-ix

Logic and regular cost functions (PDF)

Thomas Colcombet , IRIF, CNRS and Université Paris Diderot - 7, France
pp. 1-4

Algorithms for some infinite-state MDPs and stochastic games (PDF)

Kousha Etessami , School of Informatics, University Edinburgh, UK
pp. 1

Linear combinations of unordered data vectors (Abstract)

Piotr Hofman , University of Warsaw, Poland
Jerome Leroux , LaBRI, University of Bordeaux, Talence, France
Patrick Totzke , University of Edinburgh, UK
pp. 1-11

An interpretation of system F through bar recursion (Abstract)

Valentin Blot , Queen Mary University of London, UK
pp. 1-12

On the extension of computable real functions (Abstract)

Mathieu Hoyrup , Université de Lorraine, CNRS, Inria, LORIA, F 54000 Nancy, France
Walid Gomaa , Egypt Japan University of Science and Technology, Faculty of Engineering, Alexandria University, Egypt
pp. 1-12

Logics for continuous reachability in Petri nets and vector addition systems with states (Abstract)

Michael Blondin , Technische Universität München, Germany
Christoph Haase , University of Oxford, United Kingdom
pp. 1-12

Foundation for a series of efficient simulation algorithms (Abstract)

Gerard Cece , FEMTO-ST Institute/CNRS, Univ. Bourgogne Franche-Comté, Montbéliard, France
pp. 1-12

Separation for dot-depth two (Abstract)

Thomas Place , LaBRI, Bordeaux University, France
Marc Zeitoun , LaBRI, Bordeaux University, France
pp. 1-12

Foundational nonuniform (Co)datatypes for higher-order logic (Abstract)

Jasmin Christian Blanchette , Vrije Universiteit Amsterdam, The Netherlands
Fabian Meier , Institute of Information Security, Department of Computer Science, ETH Zürich, Switzerland
Andrei Popescu , School of Science and Technology, Middlesex University London, UK
Dmitriy Traytel , Institute of Information Security, Department of Computer Science, ETH Zürich, Switzerland
pp. 1-12

Common knowledge and multi-scale locality analysis in Cayley structures (Abstract)

Felix Canavoi , TU Darmstadt, Germany
Martin Otto , TU Darmstadt, Germany
pp. 1-12

Bar induction: The good, the bad, and the ugly (Abstract)

Vincent Rahli , SnT, University of Luxembourg, Luxembourg
Mark Bickford , Cornell University, USA
Robert L. Constable , Cornell University, USA
pp. 1-12

Constructive completeness for the linear-time μ-calculus (Abstract)

Amina Doumane , IRIF, Université Paris Diderot & LSV, ENS Paris-Saclay, Université Paris-Saclay & CNRS, France
pp. 1-12

Gödel logic: From natural deduction to parallel computation (Abstract)

Federico Aschieri , Institute of Discrete Mathematics and Geometry, TU Wien, Austria
Agata Ciabattoni , Theory and Logic Group, TU Wien, Austria
Francesco A. Genco , Theory and Logic Group, TU Wien, Austria
pp. 1-12

Higher-order parity automata (Abstract)

Paul-Andre Mellies , Institut de Recherche en Informatique Fondamentale, CNRS, Université Paris Diderot, France
pp. 1-12

Large scale geometries of infinite strings (Abstract)

Bakh Khoussainov , Department of Computer Science, The University of Auckland, New Zealand
Toru Takisaka , Research Institute for Mathematical Sciences, Kyoto University, Japan
pp. 1-12

Regular separability of one counter automata (Abstract)

Wojciech Czerwinski , University of Warsaw, Poland
Slawomir Lasota , University of Warsaw, Poland
pp. 1-12

Learning first-order definable concepts over structures of small degree (Abstract)

Martin Grohe , RWTH Aachen University, Germany
Martin Ritzert , RWTH Aachen University, Germany
pp. 1-12

Definability of summation problems for Abelian groups and semigroups (Abstract)

Faried Abu Zaid , TU Ilmenau, Germany
Anuj Dawar , University of Cambridge, UK
Erich Gradel , RWTH Aachen University, Germany
Wied Pakusa , University of Oxford, UK
pp. 1-11

Timed pushdown automata and branching vector addition systems (Abstract)

Lorenzo Clemente , Faculty of Mathematics, Informatics and Mechanics, University of Warsaw, Poland
Slawomir Lasota , Faculty of Mathematics, Informatics and Mechanics, University of Warsaw, Poland
Ranko Lazic , DIMAP, Department of Computer Science, University of Warwick, UK
Filip Mazowiecki , DIMAP, Department of Computer Science, University of Warwick, UK
pp. 1-12

Fibred fibration categories (Abstract)

Taichi Uemura , Research Institute for Mathematical Sciences, Kyoto University, Japan
pp. 1-12

The logic of counting query answers (Abstract)

Hubie Chen , Departamento LSI, Universidad del País Vasco, E-20018 San Sebastián, Spain
Stefan Mengel , CNRS, CRIL UMR 8188, France
pp. 1-12

Enumeration reducibility in closure spaces with applications to logic and algebra (Abstract)

Emmanuel Jeandel , Université de Lorraine, CNRS, Inria, LORIA, F 54000 Nancy, France
pp. 1-11

The limits of SDP relaxations for general-valued CSPs (Abstract)

Johan Thapper , Université Paris-Est, Marne-la-Vallée, France
Stanislav Zivny , University of Oxford, UK
pp. 1-12

Cut-free completeness for modal mu-calculus (Abstract)

Bahareh Afshari , Department of Computer Science and Engineering, University of Gothenburg, Rännvägen 6, S-41296 Göteborg, Sweden
Graham E. Leigh , Department of Philosophy, Linguistics, Theory of Science, University of Gothenburg, Box 200, S-40530 Göteborg, Sweden
pp. 1-12

Dual-context calculi for modal logic (Abstract)

G. A. Kavvos , Department of Computer Science, University of Oxford, UK
pp. 1-12

Computing quantiles in Markov chains with multi-dimensional costs (Abstract)

Christoph Haase , University of Oxford, UK
Stefan Kiefer , University of Oxford, UK
Markus Lohrey , Universität Siegen, Germany
pp. 1-12

Riesz Modal logic for Markov processes (Abstract)

Matteo Mio , CNRS/ENS-Lyon, France
Robert Furber , Aalborg University, Denmark
Radu Mardare , Aalborg University, Denmark
pp. 1-12

Succinct progress measures for solving parity games (Abstract)

Marcin Jurdzinski , DIMAP, Department of Computer Science, University of Warwick, UK
Ranko Lazic , DIMAP, Department of Computer Science, University of Warwick, UK
pp. 1-9

Generalised species of rigid resource terms (Abstract)

Takeshi Tsukada , University of Tokyo, Japan
Kazuyuki Asada , University of Tokyo, Japan
C.-H. Luke Ong , University of Oxford, UK
pp. 1-12

A fine-grained hierarchy of hard problems in the separated fragment (Abstract)

Marco Voigt , Max Planck Institute for Informatics, Saarland Informatics Campus, Saarbrücken, Germany
pp. 1-12

A categorical semantics for causal structure (Abstract)

Aleks Kissinger , Institute for Computing and Information Sciences, Radboud University, Netherlands
Sander Uijlen , Institute for Computing and Information Sciences, Radboud University, Netherlands
pp. 1-12

On delay and regret determinization of max-plus automata (Abstract)

Emmanuel Filiot , Université Libre de Bruxelles, Belgium
Ismael Jecker , Université Libre de Bruxelles, Belgium
Nathan Lhote , Université Libre de Bruxelles, Belgium
Guillermo A. Perez , Université Libre de Bruxelles, Belgium
Jean-Francois Raskin , Université Libre de Bruxelles, Belgium
pp. 1-12

The clocks are ticking: No more delays! (Abstract)

Patrick Bahr , IT University of Copenhagen, Denmark
Hans Bugge Grathwohl , Aarhus University, Denmark
Rasmus Ejlers Mogelberg , IT University of Copenhagen, Denmark
pp. 1-12

Revisiting reachability in timed automata (Abstract)

Karin Quaas , Universität Leipzig, Germany
Mahsa Shirmohammadi , University of Oxford, UK
James Worrell , University of Oxford, UK
pp. 1-12

Uniform, integral and efficient proofs for the determinant identities (Abstract)

Iddo Tzameret , Department of Computer Science, Royal Holloway, University of London, UK
Stephen A. Cook , Department of Computer Science, University of Toronto, Canada
pp. 1-12

Parity objectives in countable MDPs (Abstract)

Stefan Kiefer , University of Oxford, UK
Richard Mayr , University of Edinburgh, UK
Mahsa Shirmohammadi , University of Oxford, UK
Dominik Wojtczakz , University of Liverpool, UK
pp. 1-11

Polynomial automata: Zeroness and applications (Abstract)

Michael Benedikt , Department of Computer Science, University of Oxford, UK
Timothy Duff , School of Mathematics, Georgia Institute of Technology, USA
Aditya Sharad , Department of Computer Science, University of Oxford, UK
James Worrell , Department of Computer Science, University of Oxford, UK
pp. 1-12

On the axiomatizability of quantitative algebras (Abstract)

Radu Mardare , Aalborg University, Denmark
Prakash Panangaden , McGill University, Canada
Gordon Plotkin , University of Edinburgh, Scotland
pp. 1-12

Infinitary intersection types as sequences: A new answer to Klop's problem (Abstract)

Pierre Vial , IRIF and Université Paris-Diderot France
pp. 1-12

Foundations of information integration under bag semantics (Abstract)

Andre Hernich , University of Liverpool, UK
Phokion G. Kolaitis , UC Santa Cruz and IBM Research - Almaden, USA
pp. 1-12

Perfect half space games (Abstract)

Thomas Colcombet , IRIF, CNRS & Université Paris-Diderot, France
Marcin Jurdzinski , DIMAP & Dpt. of Computer Science, University of Warwick, UK
Ranko Lazic , DIMAP & Dpt. of Computer Science, University of Warwick, UK
Sylvain Schmitz , LSV, ENS Paris-Saclay & CNRS & INRIA, Université Paris-Saclay, France
pp. 1-11

The homomorphism problem for regular graph patterns (Abstract)

Miguel Romero , Simons Inst. for the Theory of Comp., Berkeley, University of California, USA
Pablo Barcelo , Center for Semantic Web Research & DCC, University of Chile, Chile
Moshe Y. Vardi , Department of Computer Science, Rice University, USA
pp. 1-12

The Weisfeiler-Leman dimension of planar graphs is at most 3 (Abstract)

Sandra Kiefer , RWTH Aachen University, Germany
Ilia Ponomarenko , Petersburg Department of V. A. Steklov, Institute of Mathematics, Russia
Pascal Schweitzer , RWTH Aachen University, Germany
pp. 1-12

Definability of semidefinite programming and lasserre lower bounds for CSPs (Abstract)

Anuj Dawar , University of Cambridge Computer Laboratory, UK
Pengming Wang , University of Cambridge Computer Laboratory, UK
pp. 1-12

A monad for full ground reference cells (Abstract)

Ohad Kammar , University of Oxford Department of Computer Science, UK
Paul B. Levy , University of Birmingham School of Computer Science, UK
Sean K. Moss , University of Cambridge, UK
Sam Staton , University of Oxford Department of Computer Science, UK
pp. 1-12

Quotients in monadic programming: Projective algebras are equivalent to coalgebras (Abstract)

Dusko Pavlovic , University of Hawaii, Honolulu, USA
Peter-Michael Seidel , University of Hawaii, Honolulu, USA
pp. 1-12

Register automata with linear arithmetic (Abstract)

Yu-Fang Chen , Institute of Information Science, Academia Sinica, Taiwan
Ondrej Lengal , FIT, Brno University of Technology, IT4Innovations Centre of Excellence, Czech Republic
Tony Tan , Department of Computer Science and Information Engineering, National Taiwan University, Taiwan
Zhilin Wu , State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, China
pp. 1-12

The geometry of concurrent interaction: Handling multiple ports by way of multiple tokens (Abstract)

Ugo Dal Lago , Università di Bologna & INRIA Sophia Antipolis, Italy
Ryo Tanaka , The University of Tokyo, Japan
Akira Yoshimizu , The University of Tokyo, Japan
pp. 1-12

An effectful way to eliminate addiction to dependence (Abstract)

Pierre-Marie Pedrot , University of Ljubljana, Slovenia
Nicolas Tabareau , INRIA, France
pp. 1-12

Equivalence of inductive definitions and cyclic proofs under arithmetic (Abstract)

Stefano Berardi , Università di Torino, Italy
Makoto Tatsuta , National Institute of Informatics / Sokendai, Tokyo, Japan
pp. 1-12

Model-checking for successor-invariant first-order formulas on graph classes of bounded expansion (Abstract)

Jan van den Heuvel , Department of Mathematics, London School of Economics and Political Science, Houghton Street, WC2A 2AE, United Kingdom
Stephan Kreutzer , Logic and Semantics, Technische Universität Berlin, Ernst-Reuter-Platz 7, 10587, Germany
Michal Pilipczuk , Institute of Informatics, University of Warsaw, ul. Banacha 2, 02-097, Poland
Daniel A. Quiroz , Department of Mathematics, London School of Economics and Political Science, Houghton Street, WC2A 2AE, United Kingdom
Roman Rabinovich , Logic and Semantics, Technische Universität Berlin, Ernst-Reuter-Platz 7, 10587, Germany
Sebastian Siebertz , Institute of Informatics, University of Warsaw, ul. Banacha 2, 02-097, Poland
pp. 1-11

The complexity of minimal inference problem for conservative constraint languages (Abstract)

Michal Wrona , Theoretical Computer Science Department, Faculty of Mathematics and Computer Science, Jagiellonian University, Poland
pp. 1-12

Effectful applicative bisimilarity: Monads, relators, and Howe's method (Abstract)

Ugo Dal Lago , Università di Bologna & INRIA Sophia Antipolis, Italy
Francesco Gavazzo , Università di Bologna & INRIA Sophia Antipolis, Italy
Paul Blain Levy , University of Birmingham, United Kingdom
pp. 1-12

Fully abstract encodings of λ-calculus in HOcore through abstract machines (Abstract)

Malgorzata Biernacka , University of Wrocław, Poland
Dariusz Biernacki , University of Wrocław, Poland
Serguei Lenglet , Université de Lorraine, France
Piotr Polesiuk , University of Wrocław, Poland
Damien Pous , Univ. Lyon, CNRS, ENS de Lyon, UCB Lyon 1, France
Alan Schmitt , Inria, France
pp. 1-12

The continuity of monadic stream functions (Abstract)

Venanzio Capretta , School of Computer Science, University of Nottingham, UK
Jonathan Fowler , School of Computer Science, University of Nottingham, UK
pp. 1-12

A cartesian-closed category for higher-order model checking (Abstract)

Martin Hofmann , LMU Munich, Germany
Jeremy Ledent , LIX, École Polytechnique, France
pp. 1-12

Understanding the complexity of #SAT using knowledge compilation (Abstract)

Florent Capelli , Birkbeck College, University of London, UK
pp. 1-10

The primitivity of operators in the algebra of binary relations under conjunctions of containments (Abstract)

Dimitri Surinx , Hasselt University, Belgium
Jan Van den Bussche , Hasselt University, Belgium
Dirk Van Gucht , Indiana University, USA
pp. 1-10

Capturing polynomial time using Modular Decomposition (Abstract)

Berit Grussien , Department of Computer Science, Humboldt University Berlin, Germany
pp. 1-12

A type-theoretical definition of weak ω-categories (Abstract)

Eric Finster , École Polytechnique, 91192 Palaiseau France
Samuel Mimram , École Polytechnique, 91192 Palaiseau France
pp. 1-12

Games with costs and delays (Abstract)

Martin Zimmermann , Reactive Systems Group, Saarland University, 66123 Saarbrücken, Germany
pp. 1-12

Verification of randomized security protocols (Abstract)

Rohit Chadha , University of Missouri, Columbia, USA
A. Prasad Sistla , University of Illinois, Chicago, USA
Mahesh Viswanathan , University of Illinois, Urbana-Champaign, USA
pp. 1-12

Typability in bounded dimension (Abstract)

Andrej Dudenhefner , Faculty of Computer Science, Tecnical University Dortmund, Germany
Jakob Rehof , Faculty of Computer Science, Technical University Dortmund, Germany
pp. 1-12

The equivalence of two dichotomy conjectures for infinite domain constraint satisfaction problems (Abstract)

Libor Barto , Department of Algebra, Faculty of Mathematics and Physics, Charles University in Prague, Sokolovská 83, 186 00 Praha 8, Czech Republic
Michael Kompatscher , Institut für Computersprachen, Theory and Logic Group, Technische Universität Wien, Favoritenstrasse 9/E1852, A-1040, Austria
Miroslav Olsak , Department of Algebra, Faculty of Mathematics and Physics, Charles University in Prague, Sokolovská 83, 186 00 Praha 8, Czech Republic
Trung Van Pham , Institut für Computersprachen, Theory and Logic Group, Technische Universität Wien, Favoritenstrasse 9/E1852, A-1040, Austria
Michael Pinsker , Department of Algebra, Faculty of Mathematics and Physics, Charles University in Prague, Sokolovská 83, 186 00 Praha 8, Czech Republic
pp. 1-12

The pebbling comonad in Finite Model Theory (Abstract)

Samson Abramsky , Department of Computer Science, University of Oxford, U.K.
Anuj Dawar , Computer Laboratory, University of Cambridge, UK
Pengming Wang , Computer Laboratory, University of Cambridge, UK
pp. 1-12

Stack semantics of type theory (Abstract)

Thierry Coquand , Göteborgs Universitet, Sweden
Bassel Mannaa , IT-Universitetet i København, Denmark
Fabian Ruch , Göteborgs Universitet, Sweden
pp. 1-11

MDPs with energy-parity objectives (Abstract)

Richard Mayr , University of Edinburgh, UK
Sven Schewe , University of Liverpool, UK
Patrick Totzke , University of Edinburgh, UK
Dominik Wojtczak , University of Liverpool, UK
pp. 1-12

Partial derivatives on graphs for Kleene allegories (Abstract)

Yoshiki Nakamura , Tokyo Institute of Technology, Japan
pp. 1-12

First-order logic with counting (Abstract)

Dietrich Kuske , TU Ilmenau, Germany
Nicole Schweikardt , Humboldt-Universität zu Berlin, Germany
pp. 1-12

On strong determinacy of countable stochastic games (Abstract)

Stefan Kiefer , University of Oxford, UK
Richard Mayr , University of Edinburgh, UK
Mahsa Shirmohammadi , University of Oxford, UK
Dominik Wojtczak , University of Liverpool, UK
pp. 1-12

Domains and event structures for fusions (Abstract)

Paolo Baldan , University of Padova, Italy
Andrea Corradini , University of Pisa, Italy
Fabio Gadducci , University of Pisa, Italy
pp. 1-12

Strategy logic with imperfect information (Abstract)

Raphael Berthon , École Normale Supérieure de Rennes, France
Bastien Maubert , Università degli Studi di Napoli Federico II, Naples, Italy
Aniello Murano , Università degli Studi di Napoli Federico II, Naples, Italy
Sasha Rubin , Università degli Studi di Napoli Federico II, Naples, Italy
Moshe Y. Vardi , Rice University, Houston, Texas, USA
pp. 1-12

A convenient category for higher-order probability theory (Abstract)

Chris Heunen , University of Edinburgh, UK
Ohad Kammar , University of Oxford, UK
Sam Staton , University of Oxford, UK
Hongseok Yang , University of Oxford, UK
pp. 1-12

Untwisting two-way transducers in elementary time (Abstract)

Felix Baschenis , Université de Bordeaux, LaBRI, CNRS, France
Olivier Gauwin , Université de Bordeaux, LaBRI, CNRS, France
Anca Muscholl , Université de Bordeaux, LaBRI, CNRS, France
Gabriele Puppis , Université de Bordeaux, LaBRI, CNRS, France
pp. 1-12

Bounded time computation on metric spaces and Banach spaces (Abstract)

Matthias Schroder , Technische Universität Darmstadt, Schloßgartenstraße 7, 64289, Germany
Florian Steinberg , Technische Universität Darmstadt, Schloßgartenstraße 7, 64289, Germany
pp. 1-12

Quantifiers on languages and codensity monads (Abstract)

Mai Gehrke , IRIF, CNRS and Univ. Paris Diderot, France
Daniela Petrisan , IRIF, CNRS and Univ. Paris Diderot, France
Luca Reggio , IRIF, CNRS and Univ. Paris Diderot, France
pp. 1-12

Decidability, complexity, and expressiveness of first-order logic over the subword ordering (Abstract)

Simon Halfon , Lab. Specification & Verification (LSV), CNRS & ENS Paris-Saclay, Cachan, France
Philippe Schnoebelen , Lab. Specification & Verification (LSV), CNRS & ENS Paris-Saclay, Cachan, France
Georg Zetzsche , Lab. Specification & Verification (LSV), CNRS & ENS Paris-Saclay, Cachan, France
pp. 1-12

Lean and full congruence formats for recursion (Abstract)

Rob van Glabbeek , Data61, CSIRO, Sydney, Australia
pp. 1-11

Differentiation in logical form (Abstract)

Abbas Edalat , Department of Computing, Imperial College London, UK
Mehrdad Maleki , Institute for Research in Fundamental Sciences (IPM), Tehran, Iran
pp. 1-12

Static analysis of deterministic negotiations (Abstract)

Javier Esparza , Technical University of Munich, Germany
Anca Muscholl , University of Bordeaux, LaBRI, France
Igor Walukiewicz , CNRS, LaBRI, University of Bordeaux, France
pp. 1-12

On shift-invariant maximal filters and hormonal cellular automata (Abstract)

Julien Cervelle , LACL - Université Paris-Est, 61 avenue du Général de Gaulle, 94010 Créteil Cedex, France
Gregory Lafitte , LIRMM - CNRS - Université de Montpellier, 161 rue Ada, 34095 Cedex 5, France
pp. 1-10

The real projective spaces in homotopy type theory (Abstract)

Ulrik Buchholtz , Technische Universität Darmstadt, Germany
Egbert Rijke , Carnegie Mellon University, USA
pp. 1-8

Data structures for quasistrict higher categories (Abstract)

Krzysztof Bar , Department of Computer Science, University of Oxford, United Kingdom
Jamie Vicary , Department of Computer Science, University of Oxford, United Kingdom
pp. 1-12

A crevice on the Crane Beach: Finite-degree predicates (Abstract)

Michael Cadilhac , WSI, Universität Tübingen, Germany
Charles Paperman , WSI, Universität Tübingen, Germany
pp. 1-9

Descriptive Complexity for counting complexity classes (Abstract)

Marcelo Arenas , Pontificia Universidad Católica de Chile, Chile
Martin Munoz , Pontificia Universidad Católica de Chile, Chile
Cristian Riveros , Pontificia Universidad Católica de Chile, Chile
pp. 1-12

Categorical liveness checking by corecursive algebras (Abstract)

Natsuki Urabe , Dept. Computer Science, The University of Tokyo, Japan
Masaki Hara , Dept. Computer Science, The University of Tokyo, Japan
Ichiro Hasuo , National Institute of Informatics, Japan
pp. 1-12

Unrestricted stone duality for Markov processes (Abstract)

Robert Furber , Aalborg University, Denmark
Dexter Kozen , Cornell University, USA
Kim Larsen , Aalborg University, Denmark
Radu Mardare , Aalborg University, Denmark
Prakash Panangaden , McGill University, Montreal, Canada
pp. 1-9

A weakest pre-expectation semantics for mixed-sign expectations (Abstract)

Benjamin Lucien Kaminski , Software Modeling and Verification Group, RWTH Aachen University, Germany
Joost-Pieter Katoen , Software Modeling and Verification Group, RWTH Aachen University, Germany
pp. 1-12
89 ms
(Ver 3.3 (11022016))