It is our pleasure to present the proceedings volume of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018), held from9th to 12th July 2018 at Oxford (UK) as part of the Federated Logic Conference (FLoC 2018).
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 ...
Cited By
-
Herrera J, Berrocal J, Forti S, Brogi A and Murillo J (2023). Continuous QoS-aware adaptation of Cloud-IoT application placements, Computing, 10.1007/s00607-023-01153-1, 105:9, (2037-2059), Online publication date: 1-Sep-2023.
- Kerjean M and Pacaud Lemay J Higher-Order Distributions for Differential Linear Logic Foundations of Software Science and Computation Structures, (330-347)
Index Terms
- Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science
Recommendations
Acceptance Rates
Year | Submitted | Accepted | Rate |
---|---|---|---|
LICS '20 | 174 | 69 | 40% |
CSL-LICS '14 | 212 | 74 | 35% |
Overall | 386 | 143 | 37% |