LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

Full Citation in the ACM Digital Library

Black Ninjas in the Dark: Formal Analysis of Population Protocols

In this interactive paper, which you should preferably read connected to the Internet, the Black Ninjas introduce you to population protocols, a fundamental model of distributed computation, and to recent work by the authors and their colleagues on ...

Inner Models of Univalence

We present a simple inner model construction for dependent type theory, which preserves univalence.

Continuous Reasoning: Scaling the impact of formal methods

This paper describes work in continuous reasoning, where formal reasoning about a (changing) codebase is done in a fashion which mirrors the iterative, continuous model of software development that is increasingly practiced in industry. We suggest that ...

Quasi-Open Bisimilarity with Mismatch is Intuitionistic

Quasi-open bisimilarity is the coarsest notion of bisimilarity for the π-calculus that is also a congruence. This work extends quasi-open bisimilarity to handle mismatch (guards with inequalities). This minimal extension of quasi-open bisimilarity ...

Distribution-based objectives for Markov Decision Processes

We consider distribution-based objectives for Markov Decision Processes (MDP). This class of objectives gives rise to an interesting trade-off between full and partial information. As in full observation, the strategy in the MDP can depend on the state ...

A Simple and Optimal Complementation Algorithm for Büchi Automata

Complementation of Büchi automata is complex as Büchi automata in general are nondeterministic. A worst-case state-space growth of O((0.76n)n) cannot be avoided. Experiments suggest that complementation algorithms perform better on average when they are ...

Syntax and Semantics of Quantitative Type Theory

We present Quantitative Type Theory, a Type Theory that records usage information for each variable in a judgement, based on a previous system by McBride. The usage information is used to give a realizability semantics using a variant of Linear ...

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

The ellipsoid method is an algorithm that solves the (weak) feasibility and linear optimization problems for convex sets by making oracle calls to their (weak) separation problem. We observe that the previously known method for showing that this ...

Impredicative Encodings of (Higher) Inductive Types

Postulating an impredicative universe in dependent type theory allows System F style encodings of finitary inductive types, but these fail to satisfy the relevant η-equalities and consequently do not admit dependent eliminators. To recover η and ...

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

The paper deals with finite-state Markov decision processes (MDPs) with integer weights assigned to each state-action pair. New algorithms are presented to classify end components according to their limiting behavior with respect to the accumulated ...

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

We describe a dependent type theory, and a denotational model for it, that incorporates both intensional and extensional semantic universes. In the former, terms and types are interpreted as strategies on certain graph games, which are concrete data ...

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

The logic MMSNP is a restricted fragment of existential second-order logic which allows to express many interesting queries in graph theory and finite model theory. The logic was introduced by Feder and Vardi who showed that every MMSNP sentence is ...

A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow

Information-flow security is important to the safety and privacy of cyber-physical systems (CPSs) across many domains: information leakage can both violate user privacy and reveal vulnerabilities to physical attacks. CPSs face the challenge that ...

Regular and First-Order List Functions

We define two classes of functions, called regular (respectively, first-order) list functions, which manipulate objects such as lists, lists of lists, pairs of lists, lists of pairs of lists, etc. The definition is in the style of regular expressions: ...

Definable decompositions for graphs of bounded linear cliquewidth

We prove that for every positive integer k, there exists an MSO1-transduction that given a graph of linear cliquewidth at most k outputs, nondeterministically, some clique decomposition of the graph of width bounded by a function of k. A direct ...

On computability and tractability for infinite sets

We propose a definition for computable functions on hereditarily definable sets. Such sets are possibly infinite data structures that can be defined using a fixed underlying logical structure, such as (N, =). We show that, under suitable assumptions on ...

Automaton-Based Criteria for Membership in CTL

Computation Tree Logic (CTL) is widely used in formal verification, however, unlike linear temporal logic (LTL), its connection to automata over words and trees is not yet fully understood. Moreover, the long sought connection between LTL and CTL is ...

Rewriting with Frobenius

Symmetric monoidal categories have become ubiquitous as a formal environment for the analysis of compound systems in a compositional, resource-sensitive manner using the graphical syntax of string diagrams. Recently, reasoning with string diagrams has ...

Sound up-to techniques and Complete abstract domains

Abstract interpretation is a method to automatically find invariants of programs or pieces of code whose semantics is given via least fixed-points. Up-to techniques have been introduced as enhancements of coinduction, an abstract principle to prove ...

Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS

Vector Addition Systems with States (VASS) provide a well-known and fundamental model for the analysis of concurrent processes, parameterized systems, and are also used as abstract models of programs in resource bound analysis. In this paper we study ...

Concurrency and Probability: Removing Confusion, Compositionally

Assigning a satisfactory truly concurrent semantics to Petri nets with confusion and distributed decisions is a long standing problem, especially if one wants to resolve decisions by drawing from some probability distribution. Here we propose a general ...

Higher Groups in Homotopy Type Theory

We present a development of the theory of higher groups, including infinity groups and connective spectra, in homotopy type theory. An infinity group is simply the loops in a pointed, connected type, where the group structure comes from the structure ...

The concurrent game semantics of Probabilistic PCF

We define a new games model of Probabilistic PCF (PPCF) by enriching thin concurrent games with symmetry, recently introduced by Castellan et al, with probability. This model supports two interpretations of PPCF, one sequential and one parallel. We make ...

Tree-depth, quantifier elimination, and quantifier rank

For a class K of finite graphs we consider the following three statements. (i) K has bounded tree-depth. (ii) First-order logic FO has an effective generalized quantifier elimination on K. (iii) The parameterized model checking for FO on K is in para-...

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

The complexity of the parameterized halting problem for nondeterministic Turing machines p-Halt is known to be related to the question of whether there are logics capturing various complexity classes [10]. Among others, if p-Halt is in para-AC0, the ...

Computability Beyond Church-Turing via Choice Sequences

Church-Turing computability was extended by Brouwer who considered non-lawlike computability in the form of free choice sequences. Those are essentially unbounded sequences whose elements are chosen freely, i.e. not subject to any law. In this work we ...

On Higher Inductive Types in Cubical Type Theory

Cubical type theory provides a constructive justification to certain aspects of homotopy type theory such as Voevodsky's univalence axiom. This makes many extensionality principles, like function and propositional extensionality, directly provable in ...

Strong Sums in Focused Logic

A useful connective that has not previously been made to work in focused logic is the strong sum, a form of dependent sum that is eliminated by projection rather than pattern matching. This makes strong sums powerful, but it also creates a problem ...

Probabilistic Stable Functions on Discrete Cones are Power Series

We study the category Cstabm of measurable cones and measurable stable functions---a denotational model of an higher-order language with continuous probabilities and full recursion [7]. We look at Cstabm as a model for discrete probabilities, by showing ...

Unary negation fragment with equivalence relations has the finite model property

We consider an extension of the unary negation fragment of first-order logic in which arbitrarily many binary symbols may be required to be interpreted as equivalence relations. We show that this extension has the finite model property. More ...

Logics for Word Transductions with Synthesis

We introduce a logic, called ℒT, to express properties of transductions, i.e. binary relations from input to output (finite) words. In ℒT, the input/output dependencies are modelled via an origin function which associates to any position of the output ...

Work Analysis with Resource-Aware Session Types

While there exist several successful techniques for supporting programmers in deriving static resource bounds for sequential code, analyzing the resource usage of message-passing concurrent processes poses additional challenges. To meet these challenges,...

Regular Transducer Expressions for Regular Transformations

Functional MSO transductions, deterministic two-way transducers, as well as streaming string transducers are all equivalent models for regular functions. In this paper, we show that every regular function, either on finite words or on infinite words, ...

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

In a mean-payoff parity game, one of the two players aims both to achieve a qualitative parity objective and to minimize a quantitative long-term average of payoffs (aka. mean payoff). The game is zero-sum and hence the aim of the other player is to ...

Logical paradoxes in quantum computation

The precise features of quantum theory enabling quantum computational power are unclear. Contextuality---the denial of a notion of classical physical reality---has emerged as a promising hypothesis: e.g. Howard et al. showed that the magic states needed ...

Causal Computational Complexity of Distributed Processes

This paper studies the complexity of π-calculus processes with respect to the quantity of transitions caused by an incoming message. First we propose a typing system for integrating Bellantoni and Cook's characterisation of polynomially-bound recursive ...

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

In this paper we give a characterization of both Boolean and arithmetic circuit classes of logarithmic depth in the vein of descriptive complexity theory, i.e., the Boolean classes NC1, SAC1 and AC1 as well as their arithmetic counterparts #NC1, #SAC1 ...

Eager Functions as Processes

We study Milner's encoding of the call-by-value λ-calculus into the π-calculus. We show that, by tuning the encoding to two subcalculi of the π-calculus (Internal π and Asynchronous Local π), the equivalence on λ-terms induced by the encoding coincides ...

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

Game semantics is a rich and successful class of denotational models for programming languages. Most game models feature a rather intuitive setup, yet surprisingly difficult proofs of such basic results as associativity of composition of strategies. We ...

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

We present a unified translation of LTL formulas into deterministic Rabin automata, limit-deterministic Büchi automata, and nondeterministic Büchi automata. The translations yield automata of asymptotically optimal size (double or single exponential, ...

A Theory of Register Monitors

The task of a monitor is to watch, at run-time, the execution of a reactive system, and signal the occurrence of a safety violation in the observed sequence of events. While finite-state monitors have been studied extensively, in practice, monitoring ...

Playing with Repetitions in Data Words Using Energy Games

We introduce two-player games which build words over infinite alphabets, and we study the problem of checking the existence of winning strategies. These games are played by two players, who take turns in choosing valuations for variables ranging over an ...

The State Complexity of Alternating Automata

This paper studies the complexity of languages of finite words using automata theory. To go beyond the class of regular languages, we consider infinite automata and the notion of state complexity defined by Karp. We look at alternating automata as ...

Rational Synthesis Under Imperfect Information

In this paper, we study the rational synthesis problem for turn-based multiplayer non zero-sum games played on finite graphs for omega-regular objectives. Rationality is formalized by the concept of Nash equilibrium (NE). Contrary to previous works, we ...

Sequential Relational Decomposition

The concept of decomposition in computer science and engineering is considered a fundamental component of computational thinking and is prevalent in design of algorithms, software construction, hardware design, and more. We propose a simple and natural ...

ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency

We present ReLoC: a logic for proving refinements of programs in a language with higher-order state, fine-grained concurrency, polymorphism and recursive types. The core of our logic is a judgement e ⪯ e': τ, which expresses that a program e refines a ...

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

This paper studies quantitative refinements of Abramsky's applicative similarity and bisimilarity in the context of a generalisation of Fuzz, a call-by-value λ-calculus with a linear type system that can express program sensitivity, enriched with ...

Classical realizability as a classifier for nondeterminism

We show how the language of Krivine's classical realizability may be used to specify various forms of nondeterminism and relate them with properties of realizability models. More specifically, we introduce an abstract notion of multi-evaluation relation ...

Compositional Game Theory

We introduce open games as a compositional foundation of economic game theory. A compositional approach potentially allows methods of game theory and theoretical computer science to be applied to large-scale economic models for which standard economic ...

A Generalized Modality for Recursion

Nakano's later modality allows types to express that the output of a function does not immediately depend on its input, and thus that computing its fixpoint is safe. This idea, guarded recursion, has proved useful in various contexts, from functional ...

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

For a given set of queries (which are expressions in some query language) Q = {Q1, Q2, ... Qk} and for another query Q0 we say that Q determines Q0 if -- informally speaking -- for every database D, the information contained in the views Q(D) is ...

Two complete axiomatisations of pure-state qubit quantum computing

Categorical quantum mechanics places finite-dimensional quantum theory in the context of compact closed categories, with an emphasis on diagrammatic reasoning. In this framework, two equational diagrammatic calculi have been proposed for pure-state ...

Wreath Products of Distributive Forest Algebras

It is an open problem whether definability in Propositional Dynamic Logic (PDL) on forests is decidable. Based on an algebraic characterization by Bojańczyk, et. al., (2012) in terms of forest algebras, Straubing (2013) described an approach to PDL ...

Cellular Cohomology in Homotopy Type Theory

We present a development of cellular cohomology in homotopy type theory. Cohomology associates to each space a sequence of abelian groups capturing part of its structure, and has the advantage over homotopy groups in that these abelian groups of many ...

Polynomial Invariants for Affine Programs

We exhibit an algorithm to compute the strongest polynomial (or algebraic) invariants that hold at each location of a given affine program (i.e., a program having only non-deterministic (as opposed to conditional) branching and all of whose assignments ...

Unification nets: canonical proof net quantifiers

Proof nets for MLL (unit-free Multiplicative Linear Logic) are concise graphical representations of proofs which are canonical in the sense that they abstract away syntactic redundancy such as the order of non-interacting rules. We argue that Girard's ...

Satisfiability in multi-valued circuits

Satisfiability of Boolean circuits is among the most known and important problems in theoretical computer science. This problem is NP-complete in general but becomes polynomial time when restricted either to monotone gates or linear gates. We go outside ...

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

We introduce the first complete and approximately universal diagrammatic language for quantum mechanics. We make the ZX-Calculus, a diagrammatic language introduced by Coecke and Duncan, complete for the so-called Clifford+T quantum mechanics by adding ...

Diagrammatic Reasoning beyond Clifford+T Quantum Mechanics

The ZX-Calculus is a graphical language for diagrammatic reasoning in quantum mechanics and quantum information theory. An axiomatisation has recently been proven to be complete for an approximatively universal fragment of quantum mechanics, the so-...

Type-two polynomial-time and restricted lookahead

This paper provides an alternate characterization of second-order polynomial-time computability, with the goal of making second-order complexity theory more approachable. We rely on the usual oracle machines to model programs with subroutine calls. In ...

A Logical Account for Linear Partial Differential Equations

Differential Linear Logic (DiLL), introduced by Ehrhard and Regnier, extends linear logic with a notion of linear approximation of proofs. While DiLL is classical logic, i.e. has an involutive negation, classical denotational models of it in which this ...

Free Higher Groups in Homotopy Type Theory

Given a type A in homotopy type theory (HoTT), we can define the free ∞-group on A as the loop space of the suspension of A + 1. Equivalently, this free higher group can be defined as a higher inductive type F(A) with constructors unit: F(A), cons: A~F(...

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

We present the conditional value-at-risk (CVaR) in the context of Markov chains and Markov decision processes with reachability and mean-payoff objectives. CVaR quantifies risk by means of the expectation of the worst p-quantile. As such it can be used ...

Weighted model counting beyond two-variable logic

It was recently shown by van den Broeck at al. that the symmetric weighted first-order model counting problem (WFOMC) for sentences of two-variable logic FO2 is in polynomial time, while it is #P1-complete for some FO3-sentences. We extend the result ...

Around Classical and Intuitionistic Linear Logics

We revisit many aspects of the syntactic relations between (variants of) classical linear logic (LL) and (variants of) intuitionistic linear logic (ILL) in the propositional setting.

On the one hand, we study different (parametric) "negative" ...

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

We present a new quasi-polynomial algorithm for solving parity games. It is based on a new bisimulation invariant measure of complexity for parity games, called the register-index, which captures the complexity of the priority assignment. For fixed ...

Probabilistic Böhm Trees and Probabilistic Separation

We study the notion of observational equivalence in the call-by-name probabilistic λ-calculus, where two terms are said observationally equivalent if under any context, their head reductions converge with the same probability. Our goal is to generalise ...

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

Linear/non-linear (LNL) models, as described by Benton, soundly model a LNL term calculus and LNL logic closely related to intuitionistic linear logic. Every such model induces a canonical enrichment that we show soundly models a LNL lambda calculus for ...

Boolean-Valued Semantics for the Stochastic λ-Calculus

The ordinary untyped λ-calculus has a λ-theoretic model proposed in two related forms by Scott and Plotkin in the 1970s. Recently Scott showed how to introduce probability by extending these models with random variables. However, to reason about ...

An Algebraic Theory of Markov Processes

Markov processes are a fundamental model of probabilistic transition systems and are the underlying semantics of probabilistic programs. We give an algebraic axiomatisation of Markov processes using the framework of quantitative equational logic ...

Ribbon Tensorial Logic

We introduce a topologically-aware version of tensorial logic, called ribbon tensorial logic. To every proof of the logic, we associate a ribbon tangle which tracks the flow of tensorial negations inside the proof. The translation is functorial: it is ...

An Asynchronous Soundness Theorem for Concurrent Separation Logic

Concurrent separation logic (CSL) is a specification logic for concurrent imperative programs with shared memory and locks. In this paper, we develop a concurrent and interactive account of the logic inspired by asynchronous game semantics. To every ...

Riesz Modal Logic with Threshold Operators

We present a sound and complete axiomatisation of the Riesz modal logic extended with one inductively defined operator which allows the definition of threshold operators. This logic is capable of interpreting the bounded fragment of the logic ...

A sequent calculus with dependent types for classical arithmetic

In a recent paper [11], Herbelin developed dPAω, a calculus in which constructive proofs for the axioms of countable and dependent choices could be derived via the encoding of a proof of countable universal quantification as a stream of it components. ...

An answer to the Gamma question

We answer in this paper an open question (known as the "Gamma question"), related to the recent notion of coarse computability, which stems from complexity theory. The question was formulated by Andrews, Cai, Diamondstone, Jockusch and Lempp in "...

Dialectica models of type theory

We present two Dialectica-like constructions for models of intensional Martin-Löf type theory based on Gödel's original Dialectica interpretation and the Diller-Nahm variant, bringing dependent types to categorical proof theory. We set both ...

The Geometry of Computation-Graph Abstraction

The popular library TENSORFLOW (TF) has familiarised the mainstream of machine-learning community with programming language concepts such as data-flow computing and automatic differentiation. Additionally, it has introduced some genuinely new syntactic ...

A Fixpoint Logic and Dependent Effects for Temporal Property Verification

Existing approaches to temporal verification of higher-order functional programs have either sacrificed compositionality in favor of achieving automation or vice-versa. In this paper we present a dependent-refinement type & effect system to ensure that ...

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

We investigate efficient enumeration of answers to MSO-definable queries over trees which are subject to local updates. We exhibit an algorithm that uses an O(n) preprocessing phase and enumerates answers with O(log(n)) delay between them. When the tree ...

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

Dependent type theory allows us to write programs and to prove properties about those programs in the same language. However, some properties do not require much proof, as they are evident from a program's implementation, e.g. if a polymorphic program ...

Parameterized circuit complexity of model-checking on sparse structures

We prove that for every class ℒ of graphs with effectively bounded expansion, given a first-order sentence φ and an n-element structure A whose Gaifman graph belongs to ℒ, the question whether φ holds in A can be decided by a family of AC-circuits of ...

On the number of types in sparse graphs

We prove that for every class of graphs ℒ which is nowhere dense, as defined by Nešetřil and Ossona de Mendez [28, 29], and for every first order formula φ(x, y), whenever one draws a graph G ∈ ℒ and a subset of its nodes A, the number of subsets of A|y|...

Syntax and Semantics for Operations with Scopes

Motivated by the problem of separating syntax from semantics in programming with algebraic effects and handlers, we propose a categorical model of abstract syntax with so-called scoped operations. As a building block of a term, a scoped operation is not ...

Differential Equation Axiomatization: The Impressive Power of Differential Ghosts

We prove the completeness of an axiomatization for differential equation invariants. First, we show that the differential equation axioms in differential dynamic logic are complete for all algebraic invariants. Our proof exploits differential ghosts, ...

Allegories: decidability and graph homomorphisms

Allegories were introduced by Freyd and Scedrov; they form a fragment of Tarski's calculus of relations. We show that their equational theory is decidable by characterising it in terms of a specific class of graph homomorphisms.

We actually do so for an ...

A functional interpretation with state

We present a new variant of Gödel's functional interpretation in which extracted programs, rather than being pure terms of system T, interact with a global state. The purpose of the state is to store relevant information about the underlying ...

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

We propose LMSO, a proof system inspired from Linear Logic, as a proof-theoretical framework to extract finite-state stream transducers from linear-constructive proofs of omega-regular specifications. We advocate LMSO as a stepping stone toward semi-...

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

Though many safety-critical software systems use floating point to represent real-world input and output, the mathematical specifications of these systems' behaviors use real numbers. Significant deviations from those specifications can cause errors and ...

A General Framework for Relational Parametricity

Reynolds' original theory of relational parametricity was intended to capture the observation that polymorphically typed System F programs preserve all relations between inputs. But as Reynolds himself later showed, his theory can only be formulated in ...

Guarded Computational Type Theory

Nakano's later modality can be used to specify and define recursive functions which are causal or synchronous; in concert with a notion of clock variable, it is possible to also capture the broader class of productive (co)programs. Until now, it has ...

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

Motivated by a tight connection between Joyal's combinatorial species and quantitative models of linear logic, this paper introduces weighted generalised species (or weighted profunctors), where weights are morphisms of a given symmetric monoidal closed ...

Every λ-Term is Meaningful for the Infinitary Relational Model

Infinite types and formulas are known to have really curious and unsound behaviors. For instance, they allow to type Ω, the auto-autoapplication and they thus do not ensure any form of normalization/productivity. Moreover, in most infinitary frameworks, ...

A van Benthem Theorem for Fuzzy Modal Logic

We present a fuzzy (or quantitative) version of the van Benthem theorem, which characterizes propositional modal logic as the bisimulation-invariant fragment of first-order logic. Specifically, we consider a first-order fuzzy predicate logic along with ...

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

Building on recently established enumerative connections between lambda calculus and the theory of embedded graphs (or "maps"), this paper develops an analogy between typing (of lambda terms) and coloring (of maps). Our starting point is the classical ...

Separability by piecewise testable languages and downward closures beyond subwords

We introduce a flexible class of well-quasi-orderings (WQOs) on words that generalizes the ordering of (not necessarily contiguous) subwords. Each such WQO induces a class of piecewise testable languages (PTLs) as Boolean combinations of upward closed ...