This talk introduces Self-Proving models, a new class of models that formally prove the correctness of their outputs via an Interactive Proof system. After reviewing some related literature, I will formally define Self-Proving models and their per-input (worst-case) guarantees. I will then present algorithms for learning these models and explain how the complexity of the proof system affects the complexity of the learning algorithms. Finally, I will show experiments where Self-Proving models are trained to compute the Greatest Common Divisor of two integers, and to prove the correctness of their results to a simple verifier.

Joint work with Noga Amit, Shafi Goldwasser, and Guy N. Rothblum.

A stochastic adding machine (defined by P.R. Killeen and T.J. Taylor) is a Markov chain whose states are natural integers, which models the process of adding the number 1 but where there is a probability of failure in which a carry is not performed when necessary. In this lecture, we will talk about dynamical, spectral and probabilistic properties of extensions for the stochastic adding machine and their connections with other topics as Julia sets, Automata and Dynamical Systems on Banach spaces.

Categories with families (CwF) are perhaps the most widely used notion of models for dependent types. They can be described by an algebraic signature with dependent sorts for contexts, substitutions, types and terms, as well as a plethora of constants and equations. Unfortunately, this mix of dependent sorts and equations is particularly prone to transport hell, and in practice it is nearly impossible to prove non-trivial results using CwFs in a proof assistant. In this talk, I will present a method based on Pédrot's “prefascist sets” to strictify (nearly) all the equations of a CwF, so that they hold by definition. I will then discuss applications of this method to proofs of canonicity and normalisation by Gluing. This is joint work with Ambrus Kaposi.

Contraposition is the classical reasoning principle stating that A → B is equivalent to ¬B → ¬A. In typical presentations of classical Linear Logic, e.g. those based on sequent calculus or proof nets, contraposition has no significant computational content, as it corresponds basically to a change of notation. However, for systems in natural deduction style, contraposition exchanges the role of an assumption and a conclusion, which requires to perform a global transformation on the proof. We propose a term calculus for MELL in which contraposition is realized by an operator we dub contrasubstitution, which turns a proof “inside out” to exchange the roles of the conclusion and a specific assumption. We study the properties of this calculus, starting by confluence and strong-normalization. We identify an intuitionistic fragment and show that it simulates various existing classical calculi (such as Parigot's lambda-mu) via Danos et al.'s Q and T translations.

In description logic, the query entailment problem asks the following question: given an ABox A (i.e. basic finite structure, to be completed), an ontology T (or a TBox, a finite set of constrains), and a request q (= a conjunctive query, = a subgraph), does any structure satisfying the ABox and the ontology necessarily also satisfy the request? In ALC, the basic description logic (which is nothing more than modal logic in disguise), this problem is well understood, as it is known to be ExpTime-complete in combined complexity, and coNP-complete in data complexity (i.e. with TBox and query fixed) [Lutz '08].

However, the exact complexity for S, the extension of ALC where some roles (= binary relations) are specified to be transitive, was not known yet. The status being that the problem is coNExpTime-hard [Eiter et al. '09] and in 2ExpTime [Calvanese et al. '98]. An article of 2010 tried to close the gap in a special case, but sadly contains a technical mistake, which could not be repaired so far [personal communication].

In this seminar, we propose an alternative solution to the problem, that even works in the most general case: we prove that if the entailment does not hold, then there exists a counter-model admitting a representation of exponential size (although being most possibly infinite). Hence, we conclude that the query entailment for S is indeed coNExpTime-complete. The construction of such a counter-model elegantly implies a variant of automata over infinite trees.

This thesis discusses the paradigm of computation with partial information, which is necessitated by the infeasibility of processing massive datasets in their entirety. Traditional algorithms, which require full access to input data, become impractical for large-scale problems due to time and space constraints. Several models of computation that allow for partial or incomplete data access, such as property testing, data stream models, distributed computing, and massively parallel computing, have been proposed in the literature. This thesis deals with two models, the distributed LOCAL model and the data stream model in this paradigm.

In the LOCAL model, we extend existing frameworks for the well-studied problem of $(\Delta+1)$-proper coloring to a more generalized $k$-partial $(k+1)$-coloring problem, providing novel algorithms and complexity results. Given a $n$-node graph $G=(V,E)$, a $k$-partial $c$-coloring asks for a coloring of the vertices with colors in $\{1,\dots,c\}$, such that every vertex $v\in V$ has at least $\min\{k,\deg(v)\}$ neighbors with a color different from its own color. We extend the rounding based algorithm of Ghaffari and Kuhn (2020), to give a $O(\log n\cdot \log^3k)$ round algorithm and a $O(\log n\cdot \log^2k)$ round algorithm for $k$-partial list coloring and $k$-partial $(k+1)$-coloring respectively.

In the data stream model, we introduce the {\em certification} of solutions to computing problems when access to the input is restricted. This topic has received a lot of attention in the distributed computing setting, and we introduce it here in the context of \emph{streaming} algorithms, where the input is too large to be stored in memory. Given a property $P$, a \emph{streaming certification scheme} for $P$ is a \emph{prover-verifier} pair where the prover is a computationally unlimited but non-trustable oracle, and the verifier is a streaming algorithm. For any input, the prover provides the verifier with a \emph{certificate}. The verifier then receives its input as a stream in an adversarial order and must check whether the certificate is indeed a \emph{proof} that the input satisfies $P$. The main complexity measure for a streaming certification scheme is its \emph{space complexity}, defined as the sum of the size of the certificate provided by the oracle, and of the memory space required by the verifier. We give streaming certification schemes for several graph properties, including maximum matching, diameter, degeneracy, and coloring, with space complexity matching the requirement of \emph{semi-streaming}, i.e., with space complexity $O(n\, \mbox{polylog}\, n)$ for $n$-node graphs. For each of these properties, we provide upper and lower bounds on the space complexity of the corresponding certification schemes, many being tight up to logarithmic multiplicative factors. We also show that some graph properties are hard for streaming certification, in the sense that they cannot be certified in semi-streaming, as they require $\Omega(n^2)$-bit certificates.

The results presented in this thesis contribute to the growing body of work on algorithms for large datasets, particularly in the contexts of graph theory and distributed systems, and open new avenues for future research in computation with partial information.

Distributed computing encompasses all models where a set of computing entities have to collectively solve a problem while each detaining private inputs. This field of theoretical computer science then underlies many real situations: multi-core processors, servers and clouds, the internet, swarms of robots, cars or other intelligent objects, and any network in which entities have some kind of independence. This thesis is dedicated to studying the impact of limited bandwidth on the ability to solve “local problems” in distributed networks. More precisely, in a graph-network where the amount of information exchanged between two neighbors is limited over time, how long does it take to detect a cycle ?

First we study a state of the art algorithm for the detection of small even cycles and show that this technique becomes unefficient for bigger lengths of cycles. For any even length of cycle bigger than 10, there exists a family of graphs of growing size in which this technique cannot detect a cycle in a reasonable time.

Then, we exhibit a new algorithm that matches and extends the complexity of the previously mentioned one to all even lengths of cycles. To prove its correctness, we establish a general graph combinatorics result. It can be seen as a lower bound of the “local density” in a graph without a 2k-cycle.

Finally, we develop a new framework for quantum distributed computing: the distributed quantum Monte-Carlo amplification. It helps us quantumly speed up our even-length cycle detection algorithm. This same technique can also be applied to speed up other cycle detection problems in the litterature.

In its first part, this thesis focuses on the study of the ramified analytic hierarchy (RAH) in second-order arithmetic (PA2). The ramified analytic hierarchy was defined by Kleene in 1960. It is an adaptation of the notion of constructibility (introduced by G¨odel for set theory) to the framework of second-order arithmetic. The properties of this hierarchy, in relation to computability and to the study of set-theoretic models of PA2, have been studied in depth. It seems natural to formalize RAH in PA2 in an attempt to demonstrate that adding the axiom of choice or (a variant of) the axiom of constructibility to second-order arithmetic does not bring contradiction. However, the only written trace of such a formalization seems to be incorrect. In this thesis, we want to work on this formalization. To do this, we will work in a version of arithmetic obtained by removing the axiom of induction from the axioms of PA2. In this system, a new variant of the axiom of choice appears: we call it the axiom of collection, in reference to the homonymous axiom of set theory. It seems that this axiom has never been considered in the context of second-order logic. We show that it has good computational properties: its contrapositive is realized by the identity in classical realizability, while it is itself realized by the identity in intuitionistic realizability. In addition, we show that it is equivalent to an axiom which is well-behaved with respect to a negative translation from classical logic into intuitionistic logic. Finally, we show that this variant of the axiom of collection is weaker than a variant of the axiom of choice in intuitionistic logic. We therefore work in a theory without induction but containing the axiom of collection. We aim at studying the ramified analytic hierarchy. We show that it is a model of PA2 satisfying a strong version of the axiom of choice: the principle of the well-ordered universe. It seems that the axiom of collection is necessary to prove this result and we will thoroughly explain this intuition.
In the second part of the thesis, shorter than the first, we study extensional equality in finite type arithmetic. Higher Type Arithmetic (HA^ω) is a first-order many-sorted theory. It is a conservative extension of Heyting Arithmetic obtained by extending the syntax of terms to all of System T: the objects of interest here are the functionals of higher types. While equality between natural numbers is specified by the axioms of Peano, how can equality between functionals be defined? From this question, different versions of HA^ω arise, such as an extensional version (E-HA^ω) and an intentional version (I-HA^ω). In this work, we will see how the study of partial equivalence relations leads us to design a translation by parametricity from E-HA^ω to HA^ω.