LICS 2018 Accepted Papers

Clovis Eberhart and Tom Hirschowitz. What's in a game? A theory of game models
Karoliina Lehtinen. A modal mu perspective on solving parity games in quasipolynomial time.
Paul-André Melliès and Léo Stefanesco. An Asynchronous Soundness Theorem for Concurrent Separation Logic
Benoit Monin. An answer to the Gamma question
Matteo Mio. Riesz Modal Logic with Threshold Operators
Andreas Nuyts and Dominique Devriese. Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory
Grzegorz Głuch, Jerzy Marcinkowski and Piotr Ostropolski-Nalewaja. Can One Escape Red Chains? Regular Path Queries Determinacy is Undecidable.
Noam Zeilberger. A theory of linear typings as flows on 3-valent graphs
Romain Demangeon and Nobuko Yoshida. Causal Computational Complexity of Distributed Processes
Nadish de Silva. Logical paradoxes in quantum computation
Bruce Kapron and Florian Steinberg. Type-two polynomial-time and restricted lookahead.
Ki Yung Ahn, Ross Horne, Shang-Wei Lin and Alwen Tiu. Quasi-Open Bisimilarity with Mismatch is Intuitionistic
Thomas Leventis. Probabilistic Böhm Trees and Probabilistic Separation
Koko Muroya, Wai-Tak Cheung and Dan Ghica. The Geometry of Computation-Graph Abstraction
Amar Hadzihasanovic, Kang Feng Ng and Quanlong Wang. Two complete axiomatisations of pure-state qubit quantum computing
Paul-André Melliès. Ribbon tensorial logic
Steve Awodey, Jonas Frey and Sam Speight. Impredicative Encodings of (Higher) Inductive Types
Emmanuel Jeandel, Simon Perdrix and Renaud Vilmart. A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics
Olivier Laurent. Around Classical and Intuitionistic Linear Logics
Pierre Vial. Every λ-Term is Meaningful for the Infinitary Relational Model
Thomas Powell. A functional interpretation with state
Mikołaj Bojańczyk, Martin Grohe and Michał Pilipczuk. Definable decompositions for graphs of bounded linear cliquewidth
Michał Pilipczuk, Sebastian Siebertz and Szymon Toruńczyk. Parameterized circuit complexity of model-checking on sparse structures
Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski and Fabio Zanasi. Rewriting with Frobenius
Joel Allred and Ulrich Ultes-Nitsche. A Simple and Optimal Complementation Algorithm for Büchi Automata
Emmanuel Jeandel, Simon Perdrix and Renaud Vilmart. Diagrammatic Reasoning beyond Clifford+T Quantum Mechanics
Guillaume Geoffroy. Classical realizability as a classifier for nondeterminism
Kristina Sojakova and Patricia Johann. A General Framework for Relational Parametricity
Ehud Hrushovski, Joel Ouaknine, Amaury Pouly and James Worrell. Polynomial Invariants for Affine Programs
Udi Boker and Yariv Shaulian. Automaton-Based Criteria for Membership in CTL
Matthias Niewerth. MSO Queries on Trees: Enumerating Answers under Updates Using Forest Algebras
Karl Crary. Strong Sums in Focused Logic
Ankush Das, Jan Hoffmann and Frank Pfenning. Work Analysis with Resource-Aware Session Types
André Platzer and Yong Kiam Tan. Differential Equation Axiomatization: The Impressive Power of Differential Ghosts
Adrien Guatto. A Generalized Modality for Recursion
Francesco Gavazzo. Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances
Ulrik Buchholtz, Floris van Doorn and Egbert Rijke. Higher Groups in Homotopy Type Theory
Brandon Bohrer and André Platzer. A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow
Adrien Durier, Daniel Hirschkoff and Davide Sangiorgi. Eager Functions as Processes
Jonathan Sterling and Robert Harper. Guarded Computational Type Theory
Diego Figueira and M. Praveen. Playing with Repetitions in Data Words Using Energy Games
Yijia Chen, Moritz Mueller and Keita Yokoyama. A parameterized halting problem, the linear time hierarchy, and the MRDP theorem
Manuel Bodirsky, Florent Madelaine and Antoine Mottet. A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP
Takeshi Tsukada, Kazuyuki Asada and Luke Ong. Species, Profunctors and Taylor Expansion Weighted by SMCC--A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs--
Michael Hahn, Andreas Krebs and Howard Straubing. Wreath Products of Distributive Forest Algebras
Dominic Hughes. Unification nets: canonical proof net quantifiers
Yijia Chen and Jörg Flum. Tree depth, quantifier elimination, and quantifier rank
Javier Esparza, Jan Kretinsky and Salomon Sickert. One Theorem to Rule Them All: A Unified Translation of LTL into $\omega$-Automata
Laure Daviaud, Marcin Jurdzinski and Ranko Lazic. A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games
Mikolaj Bojanczyk, Laure Daviaud and Krishna Shankara Narayanan. Regular and First Order List Functions
Emmanuel Filiot, Raffaella Gentilini and Jean-Francois Raskin. Rational Synthesis Under Imperfect Information
Neil Ghani, Jules Hedges, Viktor Winschel and Philipp Zahn. Compositional game theory
Maciej Piróg, Tom Schrijvers, Nicolas Wu and Mauro Jaskelioff. Syntax and Semantics for Operations with Scopes
Nathanaël Fijalkow. The State Complexity of Alternating Automata
Antti Kuusisto and Carsten Lutz. Weighted model counting beyond two-variable logic
Filippo Bonchi, Pierre Ganty, Roberto Giacobazzi and Dusko Pavlovic. Sound up-to techniques and Complete abstract domains
Damien Pous and Valeria Vignudelli. Allegories: decidability and graph homomorphisms
Pawel Idziak and Jacek Krzaczkowski. Satisfiability in multi-valued circuits
Dan Frumin, Robbert Krebbers and Lars Birkedal. ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency
Radu Mardare, Prakash Panangaden, Dexter Kozen, Dana Scott, Robert Furber and Giorgio Bacci. Boolean-Valued Semantics for Stochastic Lambda-Calculus
Jan Kretinsky and Tobias Meggendorfer. Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes
Radu Mardare, Prakash Panangaden, Gordon Plotkin and Giorgio Bacci. An algebraic theory of Markov processes
Michał Pilipczuk, Sebastian Siebertz and Szymon Toruńczyk. On the number of types in sparse graphs
Arnaud Durand, Anselm Haak and Heribert Vollmer. Model-Theoretic Characterizations of Boolean and Arithmetic Circuit Classes of Small Depth
Paul Wild, Lutz Schröder, Dirk Pattinson and Barbara König. A van Benthem Theorem for Fuzzy Modal Logic
Luc Dartois, Emmanuel Filiot and Nathan Lhote. Logics for Word Transductions with Synthesis
Vrunda Dave, Paul Gastin and Krishna S. Regular Transducer Expressions for Regular Transformations over infinite words
Nicolai Kraus and Thorsten Altenkirch. Free Higher Groups in Homotopy Type Theory
Christel Baier, Nathalie Bertrand, Clemens Dubslaff, Daniel Gburek and Ocan Sankur. Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes
S. Akshay, Blaise Genest and Nikhil Vyas. Distribution-based objectives for Markov Decision Processes
Albert Atserias and Joanna Ochremiak. Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism Problem
Simon Castellan, Pierre Clairambault, Hugo Paquet and Glynn Winskel. The concurrent game semantics of Probabilistic PCF
Kuen-Bang Hou and Ulrik Buchholtz. Cellular Cohomology in Homotopy Type Theory
Robert Atkey. The Syntax and Semantics of Quantitative Type Theory
Mikołaj Bojańczyk and Szymon Toruńczyk. On computability and tractability for infinite sets
Tomas Brazdil, Krishnendu Chatterjee, Antonin Kucera, Petr Novotný, Dominik Velan and Florian Zuleger. Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS
Marie Kerjean. A Logical Account for Linear Partial Differential Equations
Benjamin Sherman, Luke Sciarappa, Michael Carbin and Adam Chlipala. Computable decision-making on the reals and other spaces via partiality and nondeterminism
Thomas Ferrère, Thomas A Henzinger and N Ege Sarac. A Theory of Register Monitors
Colin Riba and Pierre Pradic. LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic
Bert Lindenhovius, Michael Mislove and Vladimir Zamdzhiev. Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams
Thierry Coquand, Simon Huber and Anders Mörtberg. On Higher Inductive Types in Cubical Type Theory
Raphaëlle Crubillé. Probabilistic stable functions on discrete cones are power series.
Étienne Miquey. A sequent calculus with dependent types for classical arithmetic
Liron Cohen, Vincent Rahli, Mark Bickford and Robert Constable. Computability Beyond Church-Turing via Choice Sequences
Georg Zetzsche. PTL-separability and closures for WQOs on words
Roberto Bruni, Hernan Melgratti and Ugo Montanari. Concurrency and Probability: Removing Confusion, Compositionally
Dror Fried, Axel Legay, Joel Ouaknine and Moshe Y Vardi. Sequential Relational Decomposition
Yoji Nanjo, Hiroshi Unno, Eric Koskinen and Tachio Terauchi. Dependent Temporal Effects and Fixpoint Logic for Verification
Daniel Danielski and Emanuel Kieronski. Unary negation fragment with equivalence relations has the finite model property
Valentin Blot and James Laird. Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types
Sean Moss and Tamara von Glehn. Dialectica models of type theory

LICS Sponsorship

The symposium is sponsored by ACM SIGLOG and the IEEE Technical Committee on Mathematical Foundations of Computing.

  • ACM
  • IEEE

Website by Sam Staton based on a bootstrap design by Hartmut Eilers and Eric Koskinen.