ABSTRACT. Linear logic is an important logic for modelling resources and decomposing computational interpretations of proofs. Decision problems for fragments of linear logic exhibiting `infinitary' behaviour (such as exponentials) are notoriously complicated. In this work, we address the decision problems for variations of linear logic with fixed points (muMALL), in particular, recent systems based on `circular' and `non-wellfounded' reasoning. In this paper, we show that muMALL is undecidable.

More explicitly, we show that the general non-wellfounded system is Pi01-hard via a reduction to the non-halting of Minsky machines, and thus is strictly stronger than its circular counterpart (which is in Sigma01). Moreover, we show that the restriction of these systems to theorems with only the least fixed points is already Sigma01-complete via a reduction to the reachability problem of alternating vector addition systems with states. This implies that both the circular system and the finitary system (with explicit (co)induction) are Sigma01-complete.

ABSTRACT. We prove a linearity theorem for an extension of linear logic with addition and multiplication by a scalar: the proofs of some propositions in this logic are linear in the algebraic sense. This work is part of a wider research program that aims at defining a logic whose proof language is a quantum programming language.

ABSTRACT. Logical time is a partial order over events in distributed systems, constraining which events precede others. Special interest has been given to series-parallel orders since they correspond to formulas constructed via the two operations for "series" and "parallel" composition. For this reason, series-parallel orders have received attention from proof theory, leading to pomset logic, the logic BV, and their extensions. However, logical time does not always form a series-parallel order; indeed, ubiquitous structures in distributed systems are beyond current proof theoretic methods. In this paper, we explore how this restriction can be lifted. We design new logics that work directly on graphs instead of formulas, we develop their proof theory, and we show that our logics are conservative extensions of the logic BV.

ABSTRACT. Guarded type theory extends type theory with a handful of modalities and constants to encode productive recursion. While these theories have seen widespread use, the metatheory of guarded type theories, particularly guarded dependent type theories remains underdeveloped. We show that integrating Lob induction is the key obstruction to unifying guarded recursion and dependence in a well-behaved type theory and prove a no-go theorem sharply bounding such type theories.

Based on these results, we introduce GTT: a stratified guarded type theory. GTT is properly two type theories, static GTT and dynamic GTT. The former contains only propositional rules governing Lob induction but enjoys decidable type-checking while the latter extends the former with definitional equalities. Accordingly, dynamic GTT does not have decidable type-checking. We prove, however, a novel guarded canonicity theorem for dynamic GTT, showing that programs in dynamic GTT can be run. These two type theories work in concert, with users writing programs in static GTT and running them in dynamic GTT.

ABSTRACT. The encoding of proof systems and type theories in logical frameworks is key to allow the translation of proofs from one system to the other. The λΠ-calculus modulo rewriting is a powerful logical framework in which various systems have already been encoded, including type systems with an infinite hierarchy of type universes equipped with a unary successor operator and a binary max operator: Matita, Coq, Agda and Lean. However, to decide the word problem in this max-successor algebra, all the encodings proposed so far use rewriting with matching modulo associativity and commutativity (AC), which is of high complexity and difficult to integrate in usual algorithms for β-reduction and type-checking. In this paper, we show that we do not need matching modulo AC by enforcing terms to be in some special canonical form wrt associativity and commutativity, and by using rewriting rules taking advantage of this canonical form. This work has been implemented in the proof assistant Lambdapi.

ABSTRACT. Dedukti is a very expressive logical framework which unlike most frameworks, such as the Edinburgh Logical Framework (ELF), allows for the representation of computation alongside deduction. However, unlike ELF encodings, Dedukti encodings proposed until now do not feature an adequacy theorem --- i.e., a bijection between terms in the encoded system and in its encoding. Moreover, many of them also do not have a conservativity one, which compromises the ability of Dedukti to check proofs written in such encodings. We propose a different approach for Dedukti encodings which do not only allow for simpler conservativity proofs, but which also restore the adequacy of encodings. More precisely, we propose in this work adequate (and thus conservative) encodings for Functional Pure Type Systems. However, in contrast with ELF encodings, ours is computational --- that is, represents computation directly as computation. Therefore, our work is the first to present and prove correct an approach allowing for encodings that are both adequate and computational in Dedukti.

ABSTRACT. Implicit Computational Complexity (ICC) drives better understanding of complexity classes, but it also guides the development of resources-aware languages and static source code analyzers. Among the methods developed, the mwp-flow analysis certifies polynomial bounds on the size of the values manipulated by an imperative program. This result is obtained by bounding the transitions between states instead of focusing on states in isolation, as most static analyzers do, and is not concerned with termination or tight bounds on values. Those differences, along with its built-in compositionality, make the mwp-flow analysis a good target for determining how ICC-inspired techniques diverge compared with more traditional static analysis methods. This paper's contributions are three-fold: we fine-tune the internal machinery of the original analysis to make it tractable in practice; we extend the analysis to function calls and leverage its machinery to compute the result of the analysis efficiently; and we implement the resulting analysis as a lightweight tool to automatically perform data-size analysis of C programs. This documented effort prepares and enables the development of certified complexity analysis, by transforming a costly analysis into a tractable program, that furthermore decorrelates the problem of deciding if a bound exist with the problem of computing it.

ABSTRACT. A reactive system maintains an on-goint interaction with its environment. At each moment in time, the system receives from the environment an assignment to the input signals and responds with an assignment to the output signals. The system is correct with respect to a given specification if, for all environments, the infinite computation that is generated by the interaction between the system and the environment satisfies the specification. Reactive systems are modeled by transducers: finite state machines whose transitions are labeled by assignments to the input signals and whose states are labeled by assignments to the output signals. In the synthesis problem, we automatically transform a given specification into a correct transducer.

While complexity measures receive much attention in the design of algorithms, they are less explored in the context of synthesis. This is a serious drawback: just as we cannot imagine an algorithm designer that accepts a correct algorithm without checking its complexity, we cannot expect designers of reactive systems to accept synthesized systems that are only guaranteed to be correct. It is not clear, however, how to define the complexity of a transducer. Unlike the case of algorithms (or Turing machines in general), there is no "size of input" to relate to, and measures like time and space complexity are irrelevant. Indeed, we care for on-going interactions, along which the transducer reacts instantly according to its transition function. One immediate complexity measure for a transducer is its size, but many more complexity measures are of interest. The talk discusses such measures and describes how the search for optimal reactive systems affects the synthesis problem.