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

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 ...

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

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 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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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: ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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-...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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,...

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, ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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, ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 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 ...

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 ...

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-...

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 ...

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 ...

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(...

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 ...

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 ...

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" ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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. ...

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 "...

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 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 ...

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 ...

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 ...

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 ...

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 ...

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|...

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 ...

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 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 ...

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 ...

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-...

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 ...

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 ...

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 ...

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 ...

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, ...

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 ...

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 ...

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 ...