ACM/IEEE Logic in Computer Science, LICS 2018


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

One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata

Javier Esparza, Jan Kretínský, Salomon Sickert

One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata

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

Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes

Jan Kretínský, Tobias Meggendorfer

Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes

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

An Algebraic Theory of Markov Processes

Giorgio Bacci, Radu Mardare, Prakash Panangaden, Gordon D. Plotkin

An Algebraic Theory of Markov Processes

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

The State Complexity of Alternating Automata

Nathanaël Fijalkow

The State Complexity of Alternating Automata

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

Probabilistic Böhm Trees and Probabilistic Separation

Thomas Leventis

Probabilistic Böhm Trees and Probabilistic Separation

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

Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes

Christel Baier, Nathalie Bertrand, Clemens Dubslaff, Daniel Gburek, Ocan Sankur

Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes

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

Model-Theoretic Characterization of Boolean and Arithmetic Circuit Classes of Small Depth

Arnaud Durand, Anselm Haak, Heribert Vollmer

Model-Theoretic Characterization of Boolean and Arithmetic Circuit Classes of Small Depth

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

A General Framework for Relational Parametricity

Kristina Sojakova, Patricia Johann

A General Framework for Relational Parametricity

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

The Geometry of Computation-Graph Abstraction

Koko Muroya, Steven W. T. Cheung, Dan R. Ghica

The Geometry of Computation-Graph Abstraction

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

A modal μ perspective on solving parity games in quasi-polynomial time

Karoliina Lehtinen

A modal μ perspective on solving parity games in quasi-polynomial time

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

A sequent calculus with dependent types for classical arithmetic

Étienne Miquey

A sequent calculus with dependent types for classical arithmetic

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

Regular Transducer Expressions for Regular Transformations

Vrunda Dave, Paul Gastin, Shankara Narayanan Krishna

Regular Transducer Expressions for Regular Transformations

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

A pseudo-quasi-polynomial algorithm for mean-payoff parity games

Laure Daviaud, Marcin Jurdzinski, Ranko Lazic

A pseudo-quasi-polynomial algorithm for mean-payoff parity games

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

Black Ninjas in the Dark: Formal Analysis of Population Protocols

Michael Blondin, Javier Esparza, Stefan Jaax, Antonín Kucera

Black Ninjas in the Dark: Formal Analysis of Population Protocols

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

Playing with Repetitions in Data Words Using Energy Games

Diego Figueira, M. Praveen

Playing with Repetitions in Data Words Using Energy Games

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

Definable decompositions for graphs of bounded linear cliquewidth

Mikolaj Bojanczyk, Martin Grohe, Michal Pilipczuk

Definable decompositions for graphs of bounded linear cliquewidth

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

Sound up-to techniques and Complete abstract domains

Filippo Bonchi, Pierre Ganty, Roberto Giacobazzi, Dusko Pavlovic

Sound up-to techniques and Complete abstract domains

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

Rational Synthesis Under Imperfect Information

Emmanuel Filiot, Raffaella Gentilini, Jean-François Raskin

Rational Synthesis Under Imperfect Information

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

A Fixpoint Logic and Dependent Effects for Temporal Property Verification

Yoji Nanjo, Hiroshi Unno, Eric Koskinen, Tachio Terauchi

A Fixpoint Logic and Dependent Effects for Temporal Property Verification

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

The concurrent game semantics of Probabilistic PCF

Simon Castellan, Pierre Clairambault, Hugo Paquet, Glynn Winskel

The concurrent game semantics of Probabilistic PCF

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

Work Analysis with Resource-Aware Session Types

Ankush Das, Jan Hoffmann, Frank Pfenning

Work Analysis with Resource-Aware Session Types

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

LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic

Pierre Pradic, Colin Riba

LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic

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

Computable decision making on the reals and other spaces: via partiality and nondeterminism

Benjamin Sherman, Luke Sciarappa, Adam Chlipala, Michael Carbin

Computable decision making on the reals and other spaces: via partiality and nondeterminism

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

Sequential Relational Decomposition

Dror Fried, Axel Legay, Joël Ouaknine, Moshe Y. Vardi

Sequential Relational Decomposition

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

On the number of types in sparse graphs

Michal Pilipczuk, Sebastian Siebertz, Szymon Torunczyk

On the number of types in sparse graphs

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

Syntax and Semantics of Quantitative Type Theory

Robert Atkey

Syntax and Semantics of Quantitative Type Theory

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

Polynomial Invariants for Affine Programs

Ehud Hrushovski, Joël Ouaknine, Amaury Pouly, James Worrell

Polynomial Invariants for Affine Programs

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

Continuous Reasoning: Scaling the impact of formal methods

Peter W. O'Hearn

Continuous Reasoning: Scaling the impact of formal methods

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

Eager Functions as Processes

Adrien Durier, Daniel Hirschkoff, Davide Sangiorgi

Eager Functions as Processes

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

Logical paradoxes in quantum computation

Nadish de Silva

Logical paradoxes in quantum computation

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

A theory of linear typings as flows on 3-valent graphs

Noam Zeilberger

A theory of linear typings as flows on 3-valent graphs

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

Wreath Products of Distributive Forest Algebras

Michael Hahn, Andreas Krebs, Howard Straubing

Wreath Products of Distributive Forest Algebras

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

An Asynchronous Soundness Theorem for Concurrent Separation Logic

Paul-André Melliès, Léo Stefanesco

An Asynchronous Soundness Theorem for Concurrent Separation Logic

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

A parameterized halting problem, the linear time hierarchy, and the MRDP theorem

Yijia Chen, Moritz Müller, Keita Yokoyama

A parameterized halting problem, the linear time hierarchy, and the MRDP theorem

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

Parameterized circuit complexity of model-checking on sparse structures

Michal Pilipczuk, Sebastian Siebertz, Szymon Torunczyk

Parameterized circuit complexity of model-checking on sparse structures

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

Separability by piecewise testable languages and downward closures beyond subwords

Georg Zetzsche

Separability by piecewise testable languages and downward closures beyond subwords

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

MSO Queries on Trees: Enumerating Answers under Updates Using Forest Algebras

Matthias Niewerth

MSO Queries on Trees: Enumerating Answers under Updates Using Forest Algebras

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

Cellular Cohomology in Homotopy Type Theory

Ulrik Buchholtz, Kuen-Bang Hou (Favonia)

Cellular Cohomology in Homotopy Type Theory

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

Tree-depth, quantifier elimination, and quantifier rank

Yijia Chen, Jörg Flum

Tree-depth, quantifier elimination, and quantifier rank

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

Concurrency and Probability: Removing Confusion, Compositionally

Roberto Bruni, Hernán C. Melgratti, Ugo Montanari

Concurrency and Probability: Removing Confusion, Compositionally

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

Higher Groups in Homotopy Type Theory

Ulrik Buchholtz, Floris van Doorn, Egbert Rijke

Higher Groups in Homotopy Type Theory

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

Boolean-Valued Semantics for the Stochastic λ-Calculus

Giorgio Bacci, Robert Furber, Dexter Kozen, Radu Mardare, Prakash Panangaden, Dana Scott

Boolean-Valued Semantics for the Stochastic λ-Calculus

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

On Higher Inductive Types in Cubical Type Theory

Thierry Coquand, Simon Huber, Anders Mörtberg

On Higher Inductive Types in Cubical Type Theory

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

Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types

Valentin Blot, Jim Laird

Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types

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

A Logical Account for Linear Partial Differential Equations

Marie Kerjean

A Logical Account for Linear Partial Differential Equations

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

A Simple and Optimal Complementation Algorithm for Büchi Automata

Joël D. Allred, Ulrich Ultes-Nitsche

A Simple and Optimal Complementation Algorithm for Büchi Automata

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

Degrees of Relatedness: A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory

Andreas Nuyts, Dominique Devriese

Degrees of Relatedness: A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory

Details
Author Comments: This paper comes with a technical report containing technical details and non-mechanized proofs: https://arxiv.org/abs/1805.08684
Discussion Comments: 0
Sharing: Research produced no artifacts
Verification: Authors have verified information

Regular and First-Order List Functions

Mikolaj Bojanczyk, Laure Daviaud, Shankara Narayanan Krishna

Regular and First-Order List Functions

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

Strong Sums in Focused Logic

Karl Crary

Strong Sums in Focused Logic

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

Differential Equation Axiomatization: The Impressive Power of Differential Ghosts

André Platzer, Yong Kiam Tan

Differential Equation Axiomatization: The Impressive Power of Differential Ghosts

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

Compositional Game Theory

Neil Ghani, Jules Hedges, Viktor Winschel, Philipp Zahn

Compositional Game Theory

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

Probabilistic Stable Functions on Discrete Cones are Power Series

Raphaëlle Crubillé

Probabilistic Stable Functions on Discrete Cones are Power Series

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

A functional interpretation with state

Thomas Powell

A functional interpretation with state

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

Every λ-Term is Meaningful for the Infinitary Relational Model

Pierre Vial

Every λ-Term is Meaningful for the Infinitary Relational Model

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

A Theory of Register Monitors

Thomas Ferrère, Thomas A. Henzinger, N. Ege Saraç

A Theory of Register Monitors

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

Automaton-Based Criteria for Membership in CTL

Udi Boker, Yariv Shaulian

Automaton-Based Criteria for Membership in CTL

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

Riesz Modal Logic with Threshold Operators

Matteo Mio

Riesz Modal Logic with Threshold Operators

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

Two complete axiomatisations of pure-state qubit quantum computing

Amar Hadzihasanovic, Kang Feng Ng, Quanlong Wang

Two complete axiomatisations of pure-state qubit quantum computing

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

A van Benthem Theorem for Fuzzy Modal Logic

Paul Wild, Lutz Schröder, Dirk Pattinson, Barbara König

A van Benthem Theorem for Fuzzy Modal Logic

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

Computability Beyond Church-Turing via Choice Sequences

Mark Bickford, Liron Cohen, Robert L. Constable, Vincent Rahli

Computability Beyond Church-Turing via Choice Sequences

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

A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP

Manuel Bodirsky, Florent R. Madelaine, Antoine Mottet

A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP

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

A Generalized Modality for Recursion

Adrien Guatto

A Generalized Modality for Recursion

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

Impredicative Encodings of (Higher) Inductive Types

Steve Awodey, Jonas Frey, Sam Speight

Impredicative Encodings of (Higher) Inductive Types

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

Weighted model counting beyond two-variable logic

Antti Kuusisto, Carsten Lutz

Weighted model counting beyond two-variable logic

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

Causal Computational Complexity of Distributed Processes

Romain Demangeon, Nobuko Yoshida

Causal Computational Complexity of Distributed Processes

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

Diagrammatic Reasoning beyond Clifford+T Quantum Mechanics

Emmanuel Jeandel, Simon Perdrix, Renaud Vilmart

Diagrammatic Reasoning beyond Clifford+T Quantum Mechanics

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

Rewriting with Frobenius

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

Rewriting with Frobenius

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

On computability and tractability for infinite sets

Mikolaj Bojanczyk, Szymon Torunczyk

On computability and tractability for infinite sets

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

Logics for Word Transductions with Synthesis

Luc Dartois, Emmanuel Filiot, Nathan Lhote

Logics for Word Transductions with Synthesis

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

Unification nets: canonical proof net quantifiers

Dominic J. D. Hughes

Unification nets: canonical proof net quantifiers

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

Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism Problem

Albert Atserias, Joanna Ochremiak

Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism Problem

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

A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics

Emmanuel Jeandel, Simon Perdrix, Renaud Vilmart

A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics

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

Type-two polynomial-time and restricted lookahead

Bruce M. Kapron, Florian Steinberg

Type-two polynomial-time and restricted lookahead

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

Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances

Francesco Gavazzo

Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances

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

A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow

Brandon Bohrer, André Platzer

A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow

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

Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS

Tomás Brázdil, Krishnendu Chatterjee, Antonín Kucera, Petr Novotný, Dominik Velan, Florian Zuleger

Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS

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

Around Classical and Intuitionistic Linear Logics

Olivier Laurent

Around Classical and Intuitionistic Linear Logics

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

What's in a game?: A theory of game models

Clovis Eberhart, Tom Hirschowitz

What's in a game?: A theory of game models

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

Can One Escape Red Chains?: Regular Path Queries Determinacy is Undecidable

Grzegorz Gluch, Jerzy Marcinkowski, Piotr Ostropolski-Nalewaja

Can One Escape Red Chains?: Regular Path Queries Determinacy is Undecidable

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

Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams

Bert Lindenhovius, Michael Mislove, Vladimir Zamdzhiev

Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams

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

Species, Profunctors and Taylor Expansion Weighted by SMCC: A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs

Takeshi Tsukada, Kazuyuki Asada, C.-H. Luke Ong

Species, Profunctors and Taylor Expansion Weighted by SMCC: A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs

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

Syntax and Semantics for Operations with Scopes

Maciej Piróg, Tom Schrijvers, Nicolas Wu, Mauro Jaskelioff

Syntax and Semantics for Operations with Scopes

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

Dialectica models of type theory

Sean K. Moss, Tamara von Glehn

Dialectica models of type theory

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

ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency

Dan Frumin, Robbert Krebbers, Lars Birkedal

ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency

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

Inner Models of Univalence

Thierry Coquand

Inner Models of Univalence

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

Allegories: decidability and graph homomorphisms

Damien Pous, Valeria Vignudelli

Allegories: decidability and graph homomorphisms

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

An answer to the Gamma question

Benoit Monin

An answer to the Gamma question

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

Guarded Computational Type Theory

Jonathan Sterling, Robert Harper

Guarded Computational Type Theory

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

Satisfiability in multi-valued circuits

Pawel M. Idziak, Jacek Krzaczkowski

Satisfiability in multi-valued circuits

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

Classical realizability as a classifier for nondeterminism

Guillaume Geoffroy

Classical realizability as a classifier for nondeterminism

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

Quasi-Open Bisimilarity with Mismatch is Intuitionistic

Ross Horne, Ki Yung Ahn, Shang-Wei Lin, Alwen Tiu

Quasi-Open Bisimilarity with Mismatch is Intuitionistic

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

Free Higher Groups in Homotopy Type Theory

Nicolai Kraus, Thorsten Altenkirch

Free Higher Groups in Homotopy Type Theory

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

Distribution-based objectives for Markov Decision Processes

S. Akshay, Blaise Genest, Nikhil Vyas

Distribution-based objectives for Markov Decision Processes

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

Ribbon Tensorial Logic

Paul-André Melliès

Ribbon Tensorial Logic

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

Unary negation fragment with equivalence relations has the finite model property

Daniel Danielski, Emanuel Kieronski

Unary negation fragment with equivalence relations has the finite model property

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